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

Theorem pw2f1olem 7619
Description: Lemma for pw2f1o 7620. (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 4118 . . . . . . . . . 10  |-  ( C  e.  W  ->  C  e.  { B ,  C } )
31, 2syl 16 . . . . . . . . 9  |-  ( ph  ->  C  e.  { B ,  C } )
4 pw2f1o.2 . . . . . . . . . 10  |-  ( ph  ->  B  e.  W )
5 prid1g 4117 . . . . . . . . . 10  |-  ( B  e.  W  ->  B  e.  { B ,  C } )
64, 5syl 16 . . . . . . . . 9  |-  ( ph  ->  B  e.  { B ,  C } )
73, 6ifcld 3965 . . . . . . . 8  |-  ( ph  ->  if ( y  e.  S ,  C ,  B )  e.  { B ,  C }
)
87adantr 465 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  if ( y  e.  S ,  C ,  B )  e.  { B ,  C } )
9 eqid 2441 . . . . . . 7  |-  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B )
)  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B )
)
108, 9fmptd 6036 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) : A --> { B ,  C } )
1110adantr 465 . . . . 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 756 . . . . . 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 5703 . . . . 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 232 . . . 4  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  G : A
--> { B ,  C } )
15 iftrue 3928 . . . . . . . . 9  |-  ( x  e.  S  ->  if ( x  e.  S ,  C ,  B )  =  C )
16 pw2f1o.4 . . . . . . . . . . . 12  |-  ( ph  ->  B  =/=  C )
1716ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  /\  x  e.  A )  ->  B  =/=  C )
18 iffalse 3931 . . . . . . . . . . . 12  |-  ( -.  x  e.  S  ->  if ( x  e.  S ,  C ,  B )  =  B )
1918neeq1d 2718 . . . . . . . . . . 11  |-  ( -.  x  e.  S  -> 
( if ( x  e.  S ,  C ,  B )  =/=  C  <->  B  =/=  C ) )
2017, 19syl5ibrcom 222 . . . . . . . . . 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 2663 . . . . . . . . 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 204 . . . . . . . 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 760 . . . . . . . . . . 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 5854 . . . . . . . . . 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 3965 . . . . . . . . . . . 12  |-  ( ph  ->  if ( x  e.  S ,  C ,  B )  e.  { B ,  C }
)
2726adantr 465 . . . . . . . . . . 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 2513 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
y  e.  S  <->  x  e.  S ) )
2928ifbid 3944 . . . . . . . . . . . 12  |-  ( y  =  x  ->  if ( y  e.  S ,  C ,  B )  =  if ( x  e.  S ,  C ,  B ) )
3029, 9fvmptg 5935 . . . . . . . . . . 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 478 . . . . . . . . . 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 2482 . . . . . . . . 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 2443 . . . . . . . 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 256 . . . . . . 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 641 . . . . . 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 755 . . . . . . . 8  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  S  C_  A
)
3736sseld 3485 . . . . . . 7  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( x  e.  S  ->  x  e.  A ) )
3837pm4.71rd 635 . . . . . 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 5717 . . . . . . . 8  |-  ( G : A --> { B ,  C }  ->  G  Fn  A )
4014, 39syl 16 . . . . . . 7  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  G  Fn  A )
41 fniniseg 5989 . . . . . . 7  |-  ( G  Fn  A  ->  (
x  e.  ( `' G " { C } )  <->  ( x  e.  A  /\  ( G `  x )  =  C ) ) )
4240, 41syl 16 . . . . . 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 285 . . . . 5  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( x  e.  S  <->  x  e.  ( `' G " { C } ) ) )
4443eqrdv 2438 . . . 4  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  S  =  ( `' G " { C } ) )
4514, 44jca 532 . . 3  |-  ( (
ph  /\  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )  ->  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )
46 simprr 756 . . . . 5  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  S  =  ( `' G " { C } ) )
47 cnvimass 5343 . . . . . 6  |-  ( `' G " { C } )  C_  dom  G
48 fdm 5721 . . . . . . 7  |-  ( G : A --> { B ,  C }  ->  dom  G  =  A )
4948ad2antrl 727 . . . . . 6  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  dom  G  =  A )
5047, 49syl5sseq 3534 . . . . 5  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  ( `' G " { C }
)  C_  A )
5146, 50eqsstrd 3520 . . . 4  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  S  C_  A
)
5239ad2antrl 727 . . . . . 6  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G  Fn  A )
53 dffn5 5899 . . . . . 6  |-  ( G  Fn  A  <->  G  =  ( y  e.  A  |->  ( G `  y
) ) )
5452, 53sylib 196 . . . . 5  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G  =  ( y  e.  A  |->  ( G `  y
) ) )
55 simplrr 760 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  S  =  ( `' G " { C } ) )
5655eleq2d 2511 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
y  e.  S  <->  y  e.  ( `' G " { C } ) ) )
57 fniniseg 5989 . . . . . . . . . . . 12  |-  ( G  Fn  A  ->  (
y  e.  ( `' G " { C } )  <->  ( y  e.  A  /\  ( G `  y )  =  C ) ) )
5852, 57syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  ( y  e.  ( `' G " { C } )  <->  ( y  e.  A  /\  ( G `  y )  =  C ) ) )
5958baibd 907 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
y  e.  ( `' G " { C } )  <->  ( G `  y )  =  C ) )
6056, 59bitrd 253 . . . . . . . . 9  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
y  e.  S  <->  ( G `  y )  =  C ) )
6160biimpa 484 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  y  e.  S )  ->  ( G `  y )  =  C )
62 iftrue 3928 . . . . . . . . 9  |-  ( y  e.  S  ->  if ( y  e.  S ,  C ,  B )  =  C )
6362adantl 466 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  y  e.  S )  ->  if ( y  e.  S ,  C ,  B )  =  C )
6461, 63eqtr4d 2485 . . . . . . 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 755 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G : A
--> { B ,  C } )
6665ffvelrnda 6012 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( G `  y )  e.  { B ,  C } )
67 fvex 5862 . . . . . . . . . . . . . 14  |-  ( G `
 y )  e. 
_V
6867elpr 4028 . . . . . . . . . . . . 13  |-  ( ( G `  y )  e.  { B ,  C }  <->  ( ( G `
 y )  =  B  \/  ( G `
 y )  =  C ) )
6966, 68sylib 196 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  (
( G `  y
)  =  B  \/  ( G `  y )  =  C ) )
7069ord 377 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( -.  ( G `  y
)  =  B  -> 
( G `  y
)  =  C ) )
7170, 60sylibrd 234 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( -.  ( G `  y
)  =  B  -> 
y  e.  S ) )
7271con1d 124 . . . . . . . . 9  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( -.  y  e.  S  ->  ( G `  y
)  =  B ) )
7372imp 429 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  -.  y  e.  S )  ->  ( G `  y
)  =  B )
74 iffalse 3931 . . . . . . . . 9  |-  ( -.  y  e.  S  ->  if ( y  e.  S ,  C ,  B )  =  B )
7574adantl 466 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  /\  -.  y  e.  S )  ->  if ( y  e.  S ,  C ,  B )  =  B )
7673, 75eqtr4d 2485 . . . . . . 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 789 . . . . . 6  |-  ( ( ( ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  /\  y  e.  A )  ->  ( G `  y )  =  if ( y  e.  S ,  C ,  B ) )
7877mpteq2dva 4519 . . . . 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 2482 . . . 4  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) )
8051, 79jca 532 . . 3  |-  ( (
ph  /\  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) )  ->  ( S  C_  A  /\  G  =  ( y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )
8145, 80impbida 830 . 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 4596 . . . 4  |-  ( A  e.  V  ->  ( S  e.  ~P A  <->  S 
C_  A ) )
8482, 83syl 16 . . 3  |-  ( ph  ->  ( S  e.  ~P A 
<->  S  C_  A )
)
85 eleq1 2513 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  S  <->  y  e.  S ) )
8685ifbid 3944 . . . . . 6  |-  ( z  =  y  ->  if ( z  e.  S ,  C ,  B )  =  if ( y  e.  S ,  C ,  B ) )
8786cbvmptv 4524 . . . . 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 2455 . . 3  |-  ( ph  ->  ( G  =  ( z  e.  A  |->  if ( z  e.  S ,  C ,  B ) )  <->  G  =  (
y  e.  A  |->  if ( y  e.  S ,  C ,  B ) ) ) )
9084, 89anbi12d 710 . 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 4675 . . . 4  |-  { B ,  C }  e.  _V
92 elmapg 7431 . . . 4  |-  ( ( { B ,  C }  e.  _V  /\  A  e.  V )  ->  ( G  e.  ( { B ,  C }  ^m  A )  <->  G : A
--> { B ,  C } ) )
9391, 82, 92sylancr 663 . . 3  |-  ( ph  ->  ( G  e.  ( { B ,  C }  ^m  A )  <->  G : A
--> { B ,  C } ) )
9493anbi1d 704 . 2  |-  ( ph  ->  ( ( G  e.  ( { B ,  C }  ^m  A )  /\  S  =  ( `' G " { C } ) )  <->  ( G : A --> { B ,  C }  /\  S  =  ( `' G " { C } ) ) ) )
9581, 90, 943bitr4d 285 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 184    \/ wo 368    /\ wa 369    = wceq 1381    e. wcel 1802    =/= wne 2636   _Vcvv 3093    C_ wss 3458   ifcif 3922   ~Pcpw 3993   {csn 4010   {cpr 4012    |-> cmpt 4491   `'ccnv 4984   dom cdm 4985   "cima 4988    Fn wfn 5569   -->wf 5570   ` cfv 5574  (class class class)co 6277    ^m cmap 7418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-fv 5582  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-map 7420
This theorem is referenced by:  pw2f1o  7620  sqff1o  23321
  Copyright terms: Public domain W3C validator