Metamath Proof Explorer

Theorem infxpenc2lem2

Description: Lemma for infxpenc2 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc2.1 
|- ( ph -> A e. On )
infxpenc2.2 
|- ( ph -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
infxpenc2.3 
|- W = ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) )
infxpenc2.4 
|- ( ph -> F : ( _om ^o 2o ) -1-1-onto-> _om )
infxpenc2.5 
|- ( ph -> ( F ` (/) ) = (/) )
infxpenc2.k 
|- K = ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) )
infxpenc2.h 
|- H = ( ( ( _om CNF W ) o. K ) o. `' ( ( _om ^o 2o ) CNF W ) )
infxpenc2.l 
|- L = ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( Y o. `' X ) ) ) )
infxpenc2.x 
|- X = ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) )
infxpenc2.y 
|- Y = ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) )
infxpenc2.j 
|- J = ( ( ( _om CNF ( 2o .o W ) ) o. L ) o. `' ( _om CNF ( W .o 2o ) ) )
infxpenc2.z 
|- Z = ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) )
infxpenc2.t 
|- T = ( x e. b , y e. b |-> <. ( ( n ` b ) ` x ) , ( ( n ` b ) ` y ) >. )
infxpenc2.g 
|- G = ( `' ( n ` b ) o. ( ( ( H o. J ) o. Z ) o. T ) )
Assertion infxpenc2lem2 
|- ( ph -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) )

Proof

Step Hyp Ref Expression
1 infxpenc2.1 
 |-  ( ph -> A e. On )
2 infxpenc2.2 
 |-  ( ph -> A. b e. A ( _om C_ b -> E. w e. ( On \ 1o ) ( n ` b ) : b -1-1-onto-> ( _om ^o w ) ) )
3 infxpenc2.3 
 |-  W = ( `' ( x e. ( On \ 1o ) |-> ( _om ^o x ) ) ` ran ( n ` b ) )
4 infxpenc2.4 
 |-  ( ph -> F : ( _om ^o 2o ) -1-1-onto-> _om )
5 infxpenc2.5 
 |-  ( ph -> ( F ` (/) ) = (/) )
6 infxpenc2.k 
 |-  K = ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) )
7 infxpenc2.h 
 |-  H = ( ( ( _om CNF W ) o. K ) o. `' ( ( _om ^o 2o ) CNF W ) )
8 infxpenc2.l 
 |-  L = ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( Y o. `' X ) ) ) )
9 infxpenc2.x 
 |-  X = ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) )
10 infxpenc2.y 
 |-  Y = ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) )
11 infxpenc2.j 
 |-  J = ( ( ( _om CNF ( 2o .o W ) ) o. L ) o. `' ( _om CNF ( W .o 2o ) ) )
12 infxpenc2.z 
 |-  Z = ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) )
13 infxpenc2.t 
 |-  T = ( x e. b , y e. b |-> <. ( ( n ` b ) ` x ) , ( ( n ` b ) ` y ) >. )
14 infxpenc2.g 
 |-  G = ( `' ( n ` b ) o. ( ( ( H o. J ) o. Z ) o. T ) )
15 1 mptexd 
 |-  ( ph -> ( b e. A |-> G ) e. _V )
16 1 adantr 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> A e. On )
17 simprl 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> b e. A )
18 onelon 
 |-  ( ( A e. On /\ b e. A ) -> b e. On )
19 16 17 18 syl2anc 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> b e. On )
20 simprr 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> _om C_ b )
21 1 2 3 infxpenc2lem1 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( W e. ( On \ 1o ) /\ ( n ` b ) : b -1-1-onto-> ( _om ^o W ) ) )
22 21 simpld 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> W e. ( On \ 1o ) )
23 4 adantr 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> F : ( _om ^o 2o ) -1-1-onto-> _om )
24 5 adantr 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( F ` (/) ) = (/) )
25 21 simprd 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( n ` b ) : b -1-1-onto-> ( _om ^o W ) )
26 19 20 22 23 24 25 6 7 8 9 10 11 12 13 14 infxpenc 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> G : ( b X. b ) -1-1-onto-> b )
27 f1of 
 |-  ( G : ( b X. b ) -1-1-onto-> b -> G : ( b X. b ) --> b )
28 26 27 syl 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> G : ( b X. b ) --> b )
29 vex 
 |-  b e. _V
30 29 29 xpex 
 |-  ( b X. b ) e. _V
31 fex 
 |-  ( ( G : ( b X. b ) --> b /\ ( b X. b ) e. _V ) -> G e. _V )
32 28 30 31 sylancl 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> G e. _V )
33 eqid 
 |-  ( b e. A |-> G ) = ( b e. A |-> G )
34 33 fvmpt2 
 |-  ( ( b e. A /\ G e. _V ) -> ( ( b e. A |-> G ) ` b ) = G )
35 17 32 34 syl2anc 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( ( b e. A |-> G ) ` b ) = G )
36 35 f1oeq1d 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b <-> G : ( b X. b ) -1-1-onto-> b ) )
37 26 36 mpbird 
 |-  ( ( ph /\ ( b e. A /\ _om C_ b ) ) -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b )
38 37 expr 
 |-  ( ( ph /\ b e. A ) -> ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) )
39 38 ralrimiva 
 |-  ( ph -> A. b e. A ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) )
40 nfmpt1 
 |-  F/_ b ( b e. A |-> G )
41 40 nfeq2 
 |-  F/ b g = ( b e. A |-> G )
42 fveq1 
 |-  ( g = ( b e. A |-> G ) -> ( g ` b ) = ( ( b e. A |-> G ) ` b ) )
43 42 f1oeq1d 
 |-  ( g = ( b e. A |-> G ) -> ( ( g ` b ) : ( b X. b ) -1-1-onto-> b <-> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) )
44 43 imbi2d 
 |-  ( g = ( b e. A |-> G ) -> ( ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) <-> ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) ) )
45 41 44 ralbid 
 |-  ( g = ( b e. A |-> G ) -> ( A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) <-> A. b e. A ( _om C_ b -> ( ( b e. A |-> G ) ` b ) : ( b X. b ) -1-1-onto-> b ) ) )
46 15 39 45 spcedv 
 |-  ( ph -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) )