This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infxpenc2lem3

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 ` (/) ) = (/) )
Assertion infxpenc2lem3 
|- ( 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 eqid 
 |-  ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) ) = ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) )
7 eqid 
 |-  ( ( ( _om CNF W ) o. ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) ) ) o. `' ( ( _om ^o 2o ) CNF W ) ) = ( ( ( _om CNF W ) o. ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) ) ) o. `' ( ( _om ^o 2o ) CNF W ) )
8 eqid 
 |-  ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) o. `' ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) ) ) ) ) = ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) o. `' ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) ) ) ) )
9 eqid 
 |-  ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) = ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) )
10 eqid 
 |-  ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) = ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) )
11 eqid 
 |-  ( ( ( _om CNF ( 2o .o W ) ) o. ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) o. `' ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) ) ) ) ) ) o. `' ( _om CNF ( W .o 2o ) ) ) = ( ( ( _om CNF ( 2o .o W ) ) o. ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) o. `' ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) ) ) ) ) ) o. `' ( _om CNF ( W .o 2o ) ) )
12 eqid 
 |-  ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) ) = ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) )
13 eqid 
 |-  ( x e. b , y e. b |-> <. ( ( n ` b ) ` x ) , ( ( n ` b ) ` y ) >. ) = ( x e. b , y e. b |-> <. ( ( n ` b ) ` x ) , ( ( n ` b ) ` y ) >. )
14 eqid 
 |-  ( `' ( n ` b ) o. ( ( ( ( ( ( _om CNF W ) o. ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) ) ) o. `' ( ( _om ^o 2o ) CNF W ) ) o. ( ( ( _om CNF ( 2o .o W ) ) o. ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) o. `' ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) ) ) ) ) ) o. `' ( _om CNF ( W .o 2o ) ) ) ) o. ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) ) ) o. ( x e. b , y e. b |-> <. ( ( n ` b ) ` x ) , ( ( n ` b ) ` y ) >. ) ) ) = ( `' ( n ` b ) o. ( ( ( ( ( ( _om CNF W ) o. ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) ) ) o. `' ( ( _om ^o 2o ) CNF W ) ) o. ( ( ( _om CNF ( 2o .o W ) ) o. ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) ) o. `' ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) ) ) ) ) ) ) o. `' ( _om CNF ( W .o 2o ) ) ) ) o. ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) ) ) o. ( x e. b , y e. b |-> <. ( ( n ` b ) ` x ) , ( ( n ` b ) ` y ) >. ) ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 infxpenc2lem2 
 |-  ( ph -> E. g A. b e. A ( _om C_ b -> ( g ` b ) : ( b X. b ) -1-1-onto-> b ) )