Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  isomninnlem Unicode version

Theorem isomninnlem 12906
Description: Lemma for isomninn 12907. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.)
Hypothesis
Ref Expression
isomninnlem.g  |-  G  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
Assertion
Ref Expression
isomninnlem  |-  ( A  e.  V  ->  ( A  e. Omni  <->  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) ) )
Distinct variable groups:    A, f, x   
f, G, x    f, V, x

Proof of Theorem isomninnlem
Dummy variables  g  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isomnimap 6957 . 2  |-  ( A  e.  V  ->  ( A  e. Omni  <->  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) ) )
2 fveq1 5372 . . . . . . . . 9  |-  ( g  =  ( `' G  o.  f )  ->  (
g `  x )  =  ( ( `' G  o.  f ) `
 x ) )
32eqeq1d 2121 . . . . . . . 8  |-  ( g  =  ( `' G  o.  f )  ->  (
( g `  x
)  =  (/)  <->  ( ( `' G  o.  f
) `  x )  =  (/) ) )
43rexbidv 2410 . . . . . . 7  |-  ( g  =  ( `' G  o.  f )  ->  ( E. x  e.  A  ( g `  x
)  =  (/)  <->  E. x  e.  A  ( ( `' G  o.  f
) `  x )  =  (/) ) )
52eqeq1d 2121 . . . . . . . 8  |-  ( g  =  ( `' G  o.  f )  ->  (
( g `  x
)  =  1o  <->  ( ( `' G  o.  f
) `  x )  =  1o ) )
65ralbidv 2409 . . . . . . 7  |-  ( g  =  ( `' G  o.  f )  ->  ( A. x  e.  A  ( g `  x
)  =  1o  <->  A. x  e.  A  ( ( `' G  o.  f
) `  x )  =  1o ) )
74, 6orbi12d 765 . . . . . 6  |-  ( g  =  ( `' G  o.  f )  ->  (
( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o )  <-> 
( E. x  e.  A  ( ( `' G  o.  f ) `
 x )  =  (/)  \/  A. x  e.  A  ( ( `' G  o.  f ) `
 x )  =  1o ) ) )
8 simplr 502 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )
9 isomninnlem.g . . . . . . . . . . . . 13  |-  G  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
109frechashgf1o 10088 . . . . . . . . . . . 12  |-  G : om
-1-1-onto-> NN0
11 f1ocnv 5334 . . . . . . . . . . . 12  |-  ( G : om -1-1-onto-> NN0  ->  `' G : NN0
-1-1-onto-> om )
12 f1of 5321 . . . . . . . . . . . 12  |-  ( `' G : NN0 -1-1-onto-> om  ->  `' G : NN0 --> om )
1310, 11, 12mp2b 8 . . . . . . . . . . 11  |-  `' G : NN0 --> om
14 0nn0 8890 . . . . . . . . . . . 12  |-  0  e.  NN0
15 1nn0 8891 . . . . . . . . . . . 12  |-  1  e.  NN0
16 prssi 3642 . . . . . . . . . . . 12  |-  ( ( 0  e.  NN0  /\  1  e.  NN0 )  ->  { 0 ,  1 }  C_  NN0 )
1714, 15, 16mp2an 420 . . . . . . . . . . 11  |-  { 0 ,  1 }  C_  NN0
18 fssres 5254 . . . . . . . . . . 11  |-  ( ( `' G : NN0 --> om  /\  { 0 ,  1 } 
C_  NN0 )  ->  ( `' G  |`  { 0 ,  1 } ) : { 0 ,  1 } --> om )
1913, 17, 18mp2an 420 . . . . . . . . . 10  |-  ( `' G  |`  { 0 ,  1 } ) : { 0 ,  1 } --> om
20 ffn 5228 . . . . . . . . . 10  |-  ( ( `' G  |`  { 0 ,  1 } ) : { 0 ,  1 } --> om  ->  ( `' G  |`  { 0 ,  1 } )  Fn  { 0 ,  1 } )
2119, 20ax-mp 7 . . . . . . . . 9  |-  ( `' G  |`  { 0 ,  1 } )  Fn  { 0 ,  1 }
22 fvres 5397 . . . . . . . . . . 11  |-  ( j  e.  { 0 ,  1 }  ->  (
( `' G  |`  { 0 ,  1 } ) `  j
)  =  ( `' G `  j ) )
23 elpri 3514 . . . . . . . . . . . 12  |-  ( j  e.  { 0 ,  1 }  ->  (
j  =  0  \/  j  =  1 ) )
24 fveq2 5373 . . . . . . . . . . . . . 14  |-  ( j  =  0  ->  ( `' G `  j )  =  ( `' G `  0 ) )
25 0zd 8964 . . . . . . . . . . . . . . . . . 18  |-  ( T. 
->  0  e.  ZZ )
2625, 9frec2uz0d 10059 . . . . . . . . . . . . . . . . 17  |-  ( T. 
->  ( G `  (/) )  =  0 )
2726mptru 1321 . . . . . . . . . . . . . . . 16  |-  ( G `
 (/) )  =  0
28 peano1 4466 . . . . . . . . . . . . . . . . 17  |-  (/)  e.  om
29 f1ocnvfv 5632 . . . . . . . . . . . . . . . . 17  |-  ( ( G : om -1-1-onto-> NN0  /\  (/)  e.  om )  ->  ( ( G `
 (/) )  =  0  ->  ( `' G `  0 )  =  (/) ) )
3010, 28, 29mp2an 420 . . . . . . . . . . . . . . . 16  |-  ( ( G `  (/) )  =  0  ->  ( `' G `  0 )  =  (/) )
3127, 30ax-mp 7 . . . . . . . . . . . . . . 15  |-  ( `' G `  0 )  =  (/)
32 0lt2o 6290 . . . . . . . . . . . . . . 15  |-  (/)  e.  2o
3331, 32eqeltri 2185 . . . . . . . . . . . . . 14  |-  ( `' G `  0 )  e.  2o
3424, 33syl6eqel 2203 . . . . . . . . . . . . 13  |-  ( j  =  0  ->  ( `' G `  j )  e.  2o )
35 fveq2 5373 . . . . . . . . . . . . . 14  |-  ( j  =  1  ->  ( `' G `  j )  =  ( `' G `  1 ) )
36 df-1o 6265 . . . . . . . . . . . . . . . . . 18  |-  1o  =  suc  (/)
3736fveq2i 5376 . . . . . . . . . . . . . . . . 17  |-  ( G `
 1o )  =  ( G `  suc  (/) )
3828a1i 9 . . . . . . . . . . . . . . . . . . 19  |-  ( T. 
->  (/)  e.  om )
3925, 9, 38frec2uzsucd 10061 . . . . . . . . . . . . . . . . . 18  |-  ( T. 
->  ( G `  suc  (/) )  =  ( ( G `  (/) )  +  1 ) )
4039mptru 1321 . . . . . . . . . . . . . . . . 17  |-  ( G `
 suc  (/) )  =  ( ( G `  (/) )  +  1 )
4127oveq1i 5736 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  (/) )  +  1 )  =  ( 0  +  1 )
42 0p1e1 8738 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  1 )  =  1
4341, 42eqtri 2133 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  (/) )  +  1 )  =  1
4437, 40, 433eqtri 2137 . . . . . . . . . . . . . . . 16  |-  ( G `
 1o )  =  1
45 1onn 6368 . . . . . . . . . . . . . . . . 17  |-  1o  e.  om
46 f1ocnvfv 5632 . . . . . . . . . . . . . . . . 17  |-  ( ( G : om -1-1-onto-> NN0  /\  1o  e.  om )  ->  ( ( G `  1o )  =  1  ->  ( `' G `  1 )  =  1o ) )
4710, 45, 46mp2an 420 . . . . . . . . . . . . . . . 16  |-  ( ( G `  1o )  =  1  ->  ( `' G `  1 )  =  1o )
4844, 47ax-mp 7 . . . . . . . . . . . . . . 15  |-  ( `' G `  1 )  =  1o
49 1lt2o 6291 . . . . . . . . . . . . . . 15  |-  1o  e.  2o
5048, 49eqeltri 2185 . . . . . . . . . . . . . 14  |-  ( `' G `  1 )  e.  2o
5135, 50syl6eqel 2203 . . . . . . . . . . . . 13  |-  ( j  =  1  ->  ( `' G `  j )  e.  2o )
5234, 51jaoi 688 . . . . . . . . . . . 12  |-  ( ( j  =  0  \/  j  =  1 )  ->  ( `' G `  j )  e.  2o )
5323, 52syl 14 . . . . . . . . . . 11  |-  ( j  e.  { 0 ,  1 }  ->  ( `' G `  j )  e.  2o )
5422, 53eqeltrd 2189 . . . . . . . . . 10  |-  ( j  e.  { 0 ,  1 }  ->  (
( `' G  |`  { 0 ,  1 } ) `  j
)  e.  2o )
5554rgen 2457 . . . . . . . . 9  |-  A. j  e.  { 0 ,  1 }  ( ( `' G  |`  { 0 ,  1 } ) `
 j )  e.  2o
56 ffnfv 5530 . . . . . . . . 9  |-  ( ( `' G  |`  { 0 ,  1 } ) : { 0 ,  1 } --> 2o  <->  ( ( `' G  |`  { 0 ,  1 } )  Fn  { 0 ,  1 }  /\  A. j  e.  { 0 ,  1 }  (
( `' G  |`  { 0 ,  1 } ) `  j
)  e.  2o ) )
5721, 55, 56mpbir2an 907 . . . . . . . 8  |-  ( `' G  |`  { 0 ,  1 } ) : { 0 ,  1 } --> 2o
58 elmapi 6516 . . . . . . . . 9  |-  ( f  e.  ( { 0 ,  1 }  ^m  A )  ->  f : A --> { 0 ,  1 } )
5958adantl 273 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  f : A --> { 0 ,  1 } )
60 fco2 5245 . . . . . . . 8  |-  ( ( ( `' G  |`  { 0 ,  1 } ) : {
0 ,  1 } --> 2o  /\  f : A --> { 0 ,  1 } )  -> 
( `' G  o.  f ) : A --> 2o )
6157, 59, 60sylancr 408 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  ( `' G  o.  f
) : A --> 2o )
62 2onn 6369 . . . . . . . . 9  |-  2o  e.  om
6362a1i 9 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  2o  e.  om )
64 simpll 501 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  A  e.  V )
6563, 64elmapd 6508 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  (
( `' G  o.  f )  e.  ( 2o  ^m  A )  <-> 
( `' G  o.  f ) : A --> 2o ) )
6661, 65mpbird 166 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  ( `' G  o.  f
)  e.  ( 2o 
^m  A ) )
677, 8, 66rspcdva 2763 . . . . 5  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  ( E. x  e.  A  ( ( `' G  o.  f ) `  x
)  =  (/)  \/  A. x  e.  A  (
( `' G  o.  f ) `  x
)  =  1o ) )
68 nfv 1489 . . . . . . . . 9  |-  F/ x  A  e.  V
69 nfcv 2253 . . . . . . . . . 10  |-  F/_ x
( 2o  ^m  A
)
70 nfre1 2448 . . . . . . . . . . 11  |-  F/ x E. x  e.  A  ( g `  x
)  =  (/)
71 nfra1 2438 . . . . . . . . . . 11  |-  F/ x A. x  e.  A  ( g `  x
)  =  1o
7270, 71nfor 1534 . . . . . . . . . 10  |-  F/ x
( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o )
7369, 72nfralxy 2443 . . . . . . . . 9  |-  F/ x A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x
)  =  (/)  \/  A. x  e.  A  (
g `  x )  =  1o )
7468, 73nfan 1525 . . . . . . . 8  |-  F/ x
( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )
75 nfv 1489 . . . . . . . 8  |-  F/ x  f  e.  ( {
0 ,  1 }  ^m  A )
7674, 75nfan 1525 . . . . . . 7  |-  F/ x
( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )
77 simplr 502 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  f  e.  ( { 0 ,  1 }  ^m  A
) )
7877, 58syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  f : A --> { 0 ,  1 } )
79 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  x  e.  A )
8078, 79ffvelrnd 5508 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  (
f `  x )  e.  { 0 ,  1 } )
8117, 80sseldi 3059 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  (
f `  x )  e.  NN0 )
82 f1ocnvfv2 5631 . . . . . . . . . . 11  |-  ( ( G : om -1-1-onto-> NN0  /\  ( f `
 x )  e. 
NN0 )  ->  ( G `  ( `' G `  ( f `  x ) ) )  =  ( f `  x ) )
8310, 81, 82sylancr 408 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  ( G `  ( `' G `  ( f `  x ) ) )  =  ( f `  x ) )
8483adantr 272 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  (/) )  -> 
( G `  ( `' G `  ( f `
 x ) ) )  =  ( f `
 x ) )
85 fvco3 5444 . . . . . . . . . . . . . 14  |-  ( ( f : A --> { 0 ,  1 }  /\  x  e.  A )  ->  ( ( `' G  o.  f ) `  x
)  =  ( `' G `  ( f `
 x ) ) )
8678, 85sylancom 414 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  (
( `' G  o.  f ) `  x
)  =  ( `' G `  ( f `
 x ) ) )
8786eqeq1d 2121 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  (
( ( `' G  o.  f ) `  x
)  =  (/)  <->  ( `' G `  ( f `  x ) )  =  (/) ) )
8887biimpa 292 . . . . . . . . . . 11  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  (/) )  -> 
( `' G `  ( f `  x
) )  =  (/) )
8988fveq2d 5377 . . . . . . . . . 10  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  (/) )  -> 
( G `  ( `' G `  ( f `
 x ) ) )  =  ( G `
 (/) ) )
9089, 27syl6eq 2161 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  (/) )  -> 
( G `  ( `' G `  ( f `
 x ) ) )  =  0 )
9184, 90eqtr3d 2147 . . . . . . . 8  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  (/) )  -> 
( f `  x
)  =  0 )
9291exp31 359 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  (
x  e.  A  -> 
( ( ( `' G  o.  f ) `
 x )  =  (/)  ->  ( f `  x )  =  0 ) ) )
9376, 92reximdai 2502 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  ( E. x  e.  A  ( ( `' G  o.  f ) `  x
)  =  (/)  ->  E. x  e.  A  ( f `  x )  =  0 ) )
9483adantr 272 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  1o )  ->  ( G `  ( `' G `  ( f `
 x ) ) )  =  ( f `
 x ) )
9586adantr 272 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  1o )  ->  ( ( `' G  o.  f ) `
 x )  =  ( `' G `  ( f `  x
) ) )
96 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  1o )  ->  ( ( `' G  o.  f ) `
 x )  =  1o )
9795, 96eqtr3d 2147 . . . . . . . . . . 11  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  1o )  ->  ( `' G `  ( f `  x
) )  =  1o )
9897fveq2d 5377 . . . . . . . . . 10  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  1o )  ->  ( G `  ( `' G `  ( f `
 x ) ) )  =  ( G `
 1o ) )
9998, 44syl6eq 2161 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  1o )  ->  ( G `  ( `' G `  ( f `
 x ) ) )  =  1 )
10094, 99eqtr3d 2147 . . . . . . . 8  |-  ( ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  /\  (
( `' G  o.  f ) `  x
)  =  1o )  ->  ( f `  x )  =  1 )
101100ex 114 . . . . . . 7  |-  ( ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  /\  x  e.  A )  ->  (
( ( `' G  o.  f ) `  x
)  =  1o  ->  ( f `  x )  =  1 ) )
10276, 101ralimdaa 2470 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  ( A. x  e.  A  ( ( `' G  o.  f ) `  x
)  =  1o  ->  A. x  e.  A  ( f `  x )  =  1 ) )
10393, 102orim12d 758 . . . . 5  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  (
( E. x  e.  A  ( ( `' G  o.  f ) `
 x )  =  (/)  \/  A. x  e.  A  ( ( `' G  o.  f ) `
 x )  =  1o )  ->  ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) ) )
10467, 103mpd 13 . . . 4  |-  ( ( ( A  e.  V  /\  A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )  /\  f  e.  ( { 0 ,  1 }  ^m  A
) )  ->  ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )
105104ralrimiva 2477 . . 3  |-  ( ( A  e.  V  /\  A. g  e.  ( 2o 
^m  A ) ( E. x  e.  A  ( g `  x
)  =  (/)  \/  A. x  e.  A  (
g `  x )  =  1o ) )  ->  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )
106 fveq1 5372 . . . . . . . . 9  |-  ( f  =  ( G  o.  g )  ->  (
f `  x )  =  ( ( G  o.  g ) `  x ) )
107106eqeq1d 2121 . . . . . . . 8  |-  ( f  =  ( G  o.  g )  ->  (
( f `  x
)  =  0  <->  (
( G  o.  g
) `  x )  =  0 ) )
108107rexbidv 2410 . . . . . . 7  |-  ( f  =  ( G  o.  g )  ->  ( E. x  e.  A  ( f `  x
)  =  0  <->  E. x  e.  A  (
( G  o.  g
) `  x )  =  0 ) )
109106eqeq1d 2121 . . . . . . . 8  |-  ( f  =  ( G  o.  g )  ->  (
( f `  x
)  =  1  <->  (
( G  o.  g
) `  x )  =  1 ) )
110109ralbidv 2409 . . . . . . 7  |-  ( f  =  ( G  o.  g )  ->  ( A. x  e.  A  ( f `  x
)  =  1  <->  A. x  e.  A  (
( G  o.  g
) `  x )  =  1 ) )
111108, 110orbi12d 765 . . . . . 6  |-  ( f  =  ( G  o.  g )  ->  (
( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 )  <->  ( E. x  e.  A  ( ( G  o.  g ) `  x )  =  0  \/  A. x  e.  A  ( ( G  o.  g ) `  x )  =  1 ) ) )
112 simplr 502 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )
113 f1of 5321 . . . . . . . . . . . 12  |-  ( G : om -1-1-onto-> NN0  ->  G : om
--> NN0 )
11410, 113ax-mp 7 . . . . . . . . . . 11  |-  G : om
--> NN0
115 omelon 4480 . . . . . . . . . . . . 13  |-  om  e.  On
116115onelssi 4309 . . . . . . . . . . . 12  |-  ( 2o  e.  om  ->  2o  C_ 
om )
11762, 116ax-mp 7 . . . . . . . . . . 11  |-  2o  C_  om
118 fssres 5254 . . . . . . . . . . 11  |-  ( ( G : om --> NN0  /\  2o  C_  om )  -> 
( G  |`  2o ) : 2o --> NN0 )
119114, 117, 118mp2an 420 . . . . . . . . . 10  |-  ( G  |`  2o ) : 2o --> NN0
120 ffn 5228 . . . . . . . . . 10  |-  ( ( G  |`  2o ) : 2o --> NN0  ->  ( G  |`  2o )  Fn  2o )
121119, 120ax-mp 7 . . . . . . . . 9  |-  ( G  |`  2o )  Fn  2o
122 fvres 5397 . . . . . . . . . . 11  |-  ( j  e.  2o  ->  (
( G  |`  2o ) `
 j )  =  ( G `  j
) )
123 elpri 3514 . . . . . . . . . . . . 13  |-  ( j  e.  { (/) ,  1o }  ->  ( j  =  (/)  \/  j  =  1o ) )
124 df2o3 6279 . . . . . . . . . . . . 13  |-  2o  =  { (/) ,  1o }
125123, 124eleq2s 2207 . . . . . . . . . . . 12  |-  ( j  e.  2o  ->  (
j  =  (/)  \/  j  =  1o ) )
126 fveq2 5373 . . . . . . . . . . . . . 14  |-  ( j  =  (/)  ->  ( G `
 j )  =  ( G `  (/) ) )
127 c0ex 7678 . . . . . . . . . . . . . . . 16  |-  0  e.  _V
128127prid1 3593 . . . . . . . . . . . . . . 15  |-  0  e.  { 0 ,  1 }
12927, 128eqeltri 2185 . . . . . . . . . . . . . 14  |-  ( G `
 (/) )  e.  {
0 ,  1 }
130126, 129syl6eqel 2203 . . . . . . . . . . . . 13  |-  ( j  =  (/)  ->  ( G `
 j )  e. 
{ 0 ,  1 } )
131 fveq2 5373 . . . . . . . . . . . . . 14  |-  ( j  =  1o  ->  ( G `  j )  =  ( G `  1o ) )
132 1ex 7679 . . . . . . . . . . . . . . . 16  |-  1  e.  _V
133132prid2 3594 . . . . . . . . . . . . . . 15  |-  1  e.  { 0 ,  1 }
13444, 133eqeltri 2185 . . . . . . . . . . . . . 14  |-  ( G `
 1o )  e. 
{ 0 ,  1 }
135131, 134syl6eqel 2203 . . . . . . . . . . . . 13  |-  ( j  =  1o  ->  ( G `  j )  e.  { 0 ,  1 } )
136130, 135jaoi 688 . . . . . . . . . . . 12  |-  ( ( j  =  (/)  \/  j  =  1o )  ->  ( G `  j )  e.  { 0 ,  1 } )
137125, 136syl 14 . . . . . . . . . . 11  |-  ( j  e.  2o  ->  ( G `  j )  e.  { 0 ,  1 } )
138122, 137eqeltrd 2189 . . . . . . . . . 10  |-  ( j  e.  2o  ->  (
( G  |`  2o ) `
 j )  e. 
{ 0 ,  1 } )
139138rgen 2457 . . . . . . . . 9  |-  A. j  e.  2o  ( ( G  |`  2o ) `  j
)  e.  { 0 ,  1 }
140 ffnfv 5530 . . . . . . . . 9  |-  ( ( G  |`  2o ) : 2o --> { 0 ,  1 }  <->  ( ( G  |`  2o )  Fn  2o  /\  A. j  e.  2o  ( ( G  |`  2o ) `  j
)  e.  { 0 ,  1 } ) )
141121, 139, 140mpbir2an 907 . . . . . . . 8  |-  ( G  |`  2o ) : 2o --> { 0 ,  1 }
142 elmapi 6516 . . . . . . . . 9  |-  ( g  e.  ( 2o  ^m  A )  ->  g : A --> 2o )
143142adantl 273 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  g : A --> 2o )
144 fco2 5245 . . . . . . . 8  |-  ( ( ( G  |`  2o ) : 2o --> { 0 ,  1 }  /\  g : A --> 2o )  ->  ( G  o.  g ) : A --> { 0 ,  1 } )
145141, 143, 144sylancr 408 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( G  o.  g ) : A --> { 0 ,  1 } )
146 prexg 4091 . . . . . . . . . 10  |-  ( ( 0  e.  NN0  /\  1  e.  NN0 )  ->  { 0 ,  1 }  e.  _V )
14714, 15, 146mp2an 420 . . . . . . . . 9  |-  { 0 ,  1 }  e.  _V
148147a1i 9 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  { 0 ,  1 }  e.  _V )
149 simpll 501 . . . . . . . 8  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  A  e.  V )
150148, 149elmapd 6508 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  (
( G  o.  g
)  e.  ( { 0 ,  1 }  ^m  A )  <->  ( G  o.  g ) : A --> { 0 ,  1 } ) )
151145, 150mpbird 166 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( G  o.  g )  e.  ( { 0 ,  1 }  ^m  A
) )
152111, 112, 151rspcdva 2763 . . . . 5  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( E. x  e.  A  ( ( G  o.  g ) `  x
)  =  0  \/ 
A. x  e.  A  ( ( G  o.  g ) `  x
)  =  1 ) )
153 nfcv 2253 . . . . . . . . . 10  |-  F/_ x
( { 0 ,  1 }  ^m  A
)
154 nfre1 2448 . . . . . . . . . . 11  |-  F/ x E. x  e.  A  ( f `  x
)  =  0
155 nfra1 2438 . . . . . . . . . . 11  |-  F/ x A. x  e.  A  ( f `  x
)  =  1
156154, 155nfor 1534 . . . . . . . . . 10  |-  F/ x
( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 )
157153, 156nfralxy 2443 . . . . . . . . 9  |-  F/ x A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 )
15868, 157nfan 1525 . . . . . . . 8  |-  F/ x
( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )
159 nfv 1489 . . . . . . . 8  |-  F/ x  g  e.  ( 2o  ^m  A )
160158, 159nfan 1525 . . . . . . 7  |-  F/ x
( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )
161143adantr 272 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  g : A --> 2o )
162117a1i 9 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  2o  C_ 
om )
163161, 162fssd 5241 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  g : A --> om )
164 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  x  e.  A )
165163, 164ffvelrnd 5508 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
g `  x )  e.  om )
166 f1ocnvfv1 5630 . . . . . . . . . . 11  |-  ( ( G : om -1-1-onto-> NN0  /\  ( g `
 x )  e. 
om )  ->  ( `' G `  ( G `
 ( g `  x ) ) )  =  ( g `  x ) )
16710, 165, 166sylancr 408 . . . . . . . . . 10  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  ( `' G `  ( G `
 ( g `  x ) ) )  =  ( g `  x ) )
168167adantr 272 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  0 )  -> 
( `' G `  ( G `  ( g `
 x ) ) )  =  ( g `
 x ) )
169 fvco3 5444 . . . . . . . . . . . . . 14  |-  ( ( g : A --> 2o  /\  x  e.  A )  ->  ( ( G  o.  g ) `  x
)  =  ( G `
 ( g `  x ) ) )
170161, 169sylancom 414 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( G  o.  g
) `  x )  =  ( G `  ( g `  x
) ) )
171170eqeq1d 2121 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( G  o.  g ) `  x
)  =  0  <->  ( G `  ( g `  x ) )  =  0 ) )
172171biimpa 292 . . . . . . . . . . 11  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  0 )  -> 
( G `  (
g `  x )
)  =  0 )
173172fveq2d 5377 . . . . . . . . . 10  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  0 )  -> 
( `' G `  ( G `  ( g `
 x ) ) )  =  ( `' G `  0 ) )
174173, 31syl6eq 2161 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  0 )  -> 
( `' G `  ( G `  ( g `
 x ) ) )  =  (/) )
175168, 174eqtr3d 2147 . . . . . . . 8  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  0 )  -> 
( g `  x
)  =  (/) )
176175exp31 359 . . . . . . 7  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  (
x  e.  A  -> 
( ( ( G  o.  g ) `  x )  =  0  ->  ( g `  x )  =  (/) ) ) )
177160, 176reximdai 2502 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( E. x  e.  A  ( ( G  o.  g ) `  x
)  =  0  ->  E. x  e.  A  ( g `  x
)  =  (/) ) )
178167adantr 272 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  1 )  -> 
( `' G `  ( G `  ( g `
 x ) ) )  =  ( g `
 x ) )
179170eqeq1d 2121 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( G  o.  g ) `  x
)  =  1  <->  ( G `  ( g `  x ) )  =  1 ) )
180179biimpa 292 . . . . . . . . . . 11  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  1 )  -> 
( G `  (
g `  x )
)  =  1 )
181180fveq2d 5377 . . . . . . . . . 10  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  1 )  -> 
( `' G `  ( G `  ( g `
 x ) ) )  =  ( `' G `  1 ) )
182181, 48syl6eq 2161 . . . . . . . . 9  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  1 )  -> 
( `' G `  ( G `  ( g `
 x ) ) )  =  1o )
183178, 182eqtr3d 2147 . . . . . . . 8  |-  ( ( ( ( ( A  e.  V  /\  A. f  e.  ( {
0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  /\  (
( G  o.  g
) `  x )  =  1 )  -> 
( g `  x
)  =  1o )
184183ex 114 . . . . . . 7  |-  ( ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  /\  x  e.  A )  ->  (
( ( G  o.  g ) `  x
)  =  1  -> 
( g `  x
)  =  1o ) )
185160, 184ralimdaa 2470 . . . . . 6  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( A. x  e.  A  ( ( G  o.  g ) `  x
)  =  1  ->  A. x  e.  A  ( g `  x
)  =  1o ) )
186177, 185orim12d 758 . . . . 5  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  (
( E. x  e.  A  ( ( G  o.  g ) `  x )  =  0  \/  A. x  e.  A  ( ( G  o.  g ) `  x )  =  1 )  ->  ( E. x  e.  A  (
g `  x )  =  (/)  \/  A. x  e.  A  ( g `  x )  =  1o ) ) )
187152, 186mpd 13 . . . 4  |-  ( ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) )  /\  g  e.  ( 2o  ^m  A
) )  ->  ( E. x  e.  A  ( g `  x
)  =  (/)  \/  A. x  e.  A  (
g `  x )  =  1o ) )
188187ralrimiva 2477 . . 3  |-  ( ( A  e.  V  /\  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x
)  =  0  \/ 
A. x  e.  A  ( f `  x
)  =  1 ) )  ->  A. g  e.  ( 2o  ^m  A
) ( E. x  e.  A  ( g `  x )  =  (/)  \/ 
A. x  e.  A  ( g `  x
)  =  1o ) )
189105, 188impbida 568 . 2  |-  ( A  e.  V  ->  ( A. g  e.  ( 2o  ^m  A ) ( E. x  e.  A  ( g `  x
)  =  (/)  \/  A. x  e.  A  (
g `  x )  =  1o )  <->  A. f  e.  ( { 0 ,  1 }  ^m  A
) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) ) )
1901, 189bitrd 187 1  |-  ( A  e.  V  ->  ( A  e. Omni  <->  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( E. x  e.  A  ( f `  x )  =  0  \/  A. x  e.  A  ( f `  x )  =  1 ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 680    = wceq 1312   T. wtru 1313    e. wcel 1461   A.wral 2388   E.wrex 2389   _Vcvv 2655    C_ wss 3035   (/)c0 3327   {cpr 3492    |-> cmpt 3947   suc csuc 4245   omcom 4462   `'ccnv 4496    |` cres 4499    o. ccom 4501    Fn wfn 5074   -->wf 5075   -1-1-onto->wf1o 5078   ` cfv 5079  (class class class)co 5726  freccfrec 6239   1oc1o 6258   2oc2o 6259    ^m cmap 6494  Omnicomni 6952   0cc0 7541   1c1 7542    + caddc 7544   NN0cn0 8875   ZZcz 8952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-addcom 7639  ax-addass 7641  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-0id 7647  ax-rnegex 7648  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-ltadd 7655
This theorem depends on definitions:  df-bi 116  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-iord 4246  df-on 4248  df-ilim 4249  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-recs 6154  df-frec 6240  df-1o 6265  df-2o 6266  df-map 6496  df-omni 6954  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-inn 8625  df-n0 8876  df-z 8953  df-uz 9223
This theorem is referenced by:  isomninn  12907
  Copyright terms: Public domain W3C validator