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 ) )