MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pw2f1olem Structured version   Visualization version   Unicode version

Theorem pw2f1olem 7681
Description: Lemma for pw2f1o 7682. (Contributed by Mario Carneiro, 6-Oct-2014.)
Hypotheses
Ref Expression
pw2f1o.1  |-  ( ph  ->  A  e.  V )
pw2f1o.2  |-  ( ph  ->  B  e.  W )
pw2f1o.3  |-  ( ph  ->  C  e.  W )
pw2f1o.4  |-  ( ph  ->  B  =/=  C )
Assertion
Ref Expression
pw2f1olem  |-  ( ph  ->  ( ( S  e. 
~P A  /\  G  =  ( z  e.  A  |->  if ( z  e.  S ,  C ,  B ) ) )  <-> 
( G  e.  ( { B ,  C }  ^m  A )  /\  S  =  ( `' G " { C }
) ) ) )
Distinct variable groups:    z, A    z, B    z, C    z, S
Allowed substitution hints:    ph( z)    G( z)    V( z)    W( z)

Proof of Theorem pw2f1olem
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pw2f1o.3 . . . . . . . . . 10  |-  ( ph  ->  C  e.  W )
2 prid2g 4082 . . . . . . . . . 10  |-  ( C  e.  W  ->  C  e.  { B ,  C } )
31, 2syl 17 . . . . . . . . 9  |-  ( ph  ->  C  e.  { B ,  C } )
4 pw2f1o.2 . . . . . . . . . 10  |-  ( ph  ->  B  e.  W )
5 prid1g 4081 . . . . . . . . . 10  |-  ( B  e.  W  ->  B  e.  { B ,  C } )
64, 5syl 17 . . . . . . . . 9  |-  ( ph  ->  B  e.  { B ,  C } )
73, 6ifcld 3926 . . . . . . . 8  |-  ( ph  ->  if ( y  e.  S ,  C ,  B )  e.  { B ,  C }
)
87adantr 467 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  if ( y  e.  S ,  C ,  B )  e.  { B ,  C } )
9 eqid 2453 . . . . . . 7  |-  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B )
)  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B )
)
108, 9fmptd 6051 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) : A --> { B ,  C } )
1110adantr 467 . . . . 5  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B )
) : A --> { B ,  C } )
12 simprr 767 . . . . . 6  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) )
1312feq1d 5719 . . . . 5  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( G : A --> { B ,  C }  <->  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) : A --> { B ,  C } ) )
1411, 13mpbird 236 . . . 4  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  G : A
--> { B ,  C } )
15 iftrue 3889 . . . . . . . . 9  |-  ( x  e.  S  ->  if ( x  e.  S ,  C ,  B )  =  C )
16 pw2f1o.4 . . . . . . . . . . . 12  |-  ( ph  ->  B  =/=  C )
1716ad2antrr 733 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  B  =/=  C )
18 iffalse 3892 . . . . . . . . . . . 12  |-  ( -.  x  e.  S  ->  if ( x  e.  S ,  C ,  B )  =  B )
1918neeq1d 2685 . . . . . . . . . . 11  |-  ( -.  x  e.  S  -> 
( if ( x  e.  S ,  C ,  B )  =/=  C  <->  B  =/=  C ) )
2017, 19syl5ibrcom 226 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  ( -.  x  e.  S  ->  if ( x  e.  S ,  C ,  B )  =/=  C
) )
2120necon4bd 2646 . . . . . . . . 9  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  ( if ( x  e.  S ,  C ,  B )  =  C  ->  x  e.  S ) )
2215, 21impbid2 208 . . . . . . . 8  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  (
x  e.  S  <->  if (
x  e.  S ,  C ,  B )  =  C ) )
23 simplrr 772 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) )
2423fveq1d 5872 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  ( G `  x )  =  ( ( y  e.  A  |->  if ( y  e.  S ,  C ,  B )
) `  x )
)
25 id 22 . . . . . . . . . . 11  |-  ( x  e.  A  ->  x  e.  A )
263, 6ifcld 3926 . . . . . . . . . . . 12  |-  ( ph  ->  if ( x  e.  S ,  C ,  B )  e.  { B ,  C }
)
2726adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  if (
x  e.  S ,  C ,  B )  e.  { B ,  C } )
28 eleq1 2519 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
y  e.  S  <->  x  e.  S ) )
2928ifbid 3905 . . . . . . . . . . . 12  |-  ( y  =  x  ->  if ( y  e.  S ,  C ,  B )  =  if ( x  e.  S ,  C ,  B ) )
3029, 9fvmptg 5951 . . . . . . . . . . 11  |-  ( ( x  e.  A  /\  if ( x  e.  S ,  C ,  B )  e.  { B ,  C } )  ->  (
( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) `  x )  =  if ( x  e.  S ,  C ,  B ) )
3125, 27, 30syl2anr 481 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  (
( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) `  x )  =  if ( x  e.  S ,  C ,  B ) )
3224, 31eqtrd 2487 . . . . . . . . 9  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  ( G `  x )  =  if ( x  e.  S ,  C ,  B ) )
3332eqeq1d 2455 . . . . . . . 8  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  (
( G `  x
)  =  C  <->  if (
x  e.  S ,  C ,  B )  =  C ) )
3422, 33bitr4d 260 . . . . . . 7  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  (
x  e.  S  <->  ( G `  x )  =  C ) )
3534pm5.32da 647 . . . . . 6  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( (
x  e.  A  /\  x  e.  S )  <->  ( x  e.  A  /\  ( G `  x )  =  C ) ) )
36 simprl 765 . . . . . . . 8  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  S  C_  A
)
3736sseld 3433 . . . . . . 7  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( x  e.  S  ->  x  e.  A ) )
3837pm4.71rd 641 . . . . . 6  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( x  e.  S  <->  ( x  e.  A  /\  x  e.  S ) ) )
39 ffn 5733 . . . . . . . 8  |-  ( G : A --> { B ,  C }  ->  G  Fn  A )
4014, 39syl 17 . . . . . . 7  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  G  Fn  A )
41 fniniseg 6008 . . . . . . 7  |-  ( G  Fn  A  ->  (
x  e.  ( `' G " { C } )  <->  ( x  e.  A  /\  ( G `  x )  =  C ) ) )
4240, 41syl 17 . . . . . 6  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( x  e.  ( `' G " { C } )  <->  ( x  e.  A  /\  ( G `  x )  =  C ) ) )
4335, 38, 423bitr4d 289 . . . . 5  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( x  e.  S  <->  x  e.  ( `' G " { C } ) ) )
4443eqrdv 2451 . . . 4  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  S  =  ( `' G " { C } ) )
4514, 44jca 535 . . 3  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )
46 simprr 767 . . . . 5  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  S  =  ( `' G " { C } ) )
47 cnvimass 5191 . . . . . 6  |-  ( `' G " { C } )  C_  dom  G
48 fdm 5738 . . . . . . 7  |-  ( G : A --> { B ,  C }  ->  dom  G  =  A )
4948ad2antrl 735 . . . . . 6  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  dom  G  =  A )
5047, 49syl5sseq 3482 . . . . 5  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  ( `' G " { C }
)  C_  A )
5146, 50eqsstrd 3468 . . . 4  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  S  C_  A
)
5239ad2antrl 735 . . . . . 6  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G  Fn  A )
53 dffn5 5915 . . . . . 6  |-  ( G  Fn  A  <->  G  =  ( y  e.  A  |->  ( G `  y
) ) )
5452, 53sylib 200 . . . . 5  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G  =  ( y  e.  A  |->  ( G `  y
) ) )
55 simplrr 772 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  S  =  ( `' G " { C } ) )
5655eleq2d 2516 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
y  e.  S  <->  y  e.  ( `' G " { C } ) ) )
57 fniniseg 6008 . . . . . . . . . . . 12  |-  ( G  Fn  A  ->  (
y  e.  ( `' G " { C } )  <->  ( y  e.  A  /\  ( G `  y )  =  C ) ) )
5852, 57syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  ( y  e.  ( `' G " { C } )  <->  ( y  e.  A  /\  ( G `  y )  =  C ) ) )
5958baibd 921 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
y  e.  ( `' G " { C } )  <->  ( G `  y )  =  C ) )
6056, 59bitrd 257 . . . . . . . . 9  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
y  e.  S  <->  ( G `  y )  =  C ) )
6160biimpa 487 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  y  e.  S )  ->  ( G `  y )  =  C )
62 iftrue 3889 . . . . . . . . 9  |-  ( y  e.  S  ->  if ( y  e.  S ,  C ,  B )  =  C )
6362adantl 468 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  y  e.  S )  ->  if ( y  e.  S ,  C ,  B )  =  C )
6461, 63eqtr4d 2490 . . . . . . 7  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  y  e.  S )  ->  ( G `  y )  =  if ( y  e.  S ,  C ,  B ) )
65 simprl 765 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G : A
--> { B ,  C } )
6665ffvelrnda 6027 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( G `  y )  e.  { B ,  C } )
67 fvex 5880 . . . . . . . . . . . . . 14  |-  ( G `
 y )  e. 
_V
6867elpr 3988 . . . . . . . . . . . . 13  |-  ( ( G `  y )  e.  { B ,  C }  <->  ( ( G `
 y )  =  B  \/  ( G `
 y )  =  C ) )
6966, 68sylib 200 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
( G `  y
)  =  B  \/  ( G `  y )  =  C ) )
7069ord 379 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( -.  ( G `  y
)  =  B  -> 
( G `  y
)  =  C ) )
7170, 60sylibrd 238 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( -.  ( G `  y
)  =  B  -> 
y  e.  S ) )
7271con1d 128 . . . . . . . . 9  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( -.  y  e.  S  ->  ( G `  y
)  =  B ) )
7372imp 431 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  -.  y  e.  S )  ->  ( G `  y
)  =  B )
74 iffalse 3892 . . . . . . . . 9  |-  ( -.  y  e.  S  ->  if ( y  e.  S ,  C ,  B )  =  B )
7574adantl 468 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  -.  y  e.  S )  ->  if ( y  e.  S ,  C ,  B )  =  B )
7673, 75eqtr4d 2490 . . . . . . 7  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  -.  y  e.  S )  ->  ( G `  y
)  =  if ( y  e.  S ,  C ,  B )
)
7764, 76pm2.61dan 801 . . . . . 6  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( G `  y )  =  if ( y  e.  S ,  C ,  B ) )
7877mpteq2dva 4492 . . . . 5  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  ( y  e.  A  |->  ( G `
 y ) )  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) )
7954, 78eqtrd 2487 . . . 4  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) )
8051, 79jca 535 . . 3  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )
8145, 80impbida 844 . 2  |-  ( ph  ->  ( ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) )  <->  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) ) )
82 pw2f1o.1 . . . 4  |-  ( ph  ->  A  e.  V )
83 elpw2g 4569 . . . 4  |-  ( A  e.  V  ->  ( S  e.  ~P A  <->  S 
C_  A ) )
8482, 83syl 17 . . 3  |-  ( ph  ->  ( S  e.  ~P A 
<->  S  C_  A )
)
85 eleq1 2519 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  S  <->  y  e.  S ) )
8685ifbid 3905 . . . . . 6  |-  ( z  =  y  ->  if ( z  e.  S ,  C ,  B )  =  if ( y  e.  S ,  C ,  B ) )
8786cbvmptv 4498 . . . . 5  |-  ( z  e.  A  |->  if ( z  e.  S ,  C ,  B )
)  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B )
)
8887a1i 11 . . . 4  |-  ( ph  ->  ( z  e.  A  |->  if ( z  e.  S ,  C ,  B ) )  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) )
8988eqeq2d 2463 . . 3  |-  ( ph  ->  ( G  =  ( z  e.  A  |->  if ( z  e.  S ,  C ,  B ) )  <->  G  =  (
y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )
9084, 89anbi12d 718 . 2  |-  ( ph  ->  ( ( S  e. 
~P A  /\  G  =  ( z  e.  A  |->  if ( z  e.  S ,  C ,  B ) ) )  <-> 
( S  C_  A  /\  G  =  (
y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) ) )
91 prex 4645 . . . 4  |-  { B ,  C }  e.  _V
92 elmapg 7490 . . . 4  |-  ( ( { B ,  C }  e.  _V  /\  A  e.  V )  ->  ( G  e.  ( { B ,  C }  ^m  A )  <->  G : A
--> { B ,  C } ) )
9391, 82, 92sylancr 670 . . 3  |-  ( ph  ->  ( G  e.  ( { B ,  C }  ^m  A )  <->  G : A
--> { B ,  C } ) )
9493anbi1d 712 . 2  |-  ( ph  ->  ( ( G  e.  ( { B ,  C }  ^m  A )  /\  S  =  ( `' G " { C } ) )  <->  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) ) )
9581, 90, 943bitr4d 289 1  |-  ( ph  ->  ( ( S  e. 
~P A  /\  G  =  ( z  e.  A  |->  if ( z  e.  S ,  C ,  B ) ) )  <-> 
( G  e.  ( { B ,  C }  ^m  A )  /\  S  =  ( `' G " { C }
) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371    = wceq 1446    e. wcel 1889    =/= wne 2624   _Vcvv 3047    C_ wss 3406   ifcif 3883   ~Pcpw 3953   {csn 3970   {cpr 3972    |-> cmpt 4464   `'ccnv 4836   dom cdm 4837   "cima 4840    Fn wfn 5580   -->wf 5581   ` cfv 5585  (class class class)co 6295    ^m cmap 7477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7479
This theorem is referenced by:  pw2f1o  7682  sqff1o  24121
  Copyright terms: Public domain W3C validator