Metamath Proof Explorer

Theorem infxpenc

Description: A canonical version of infxpen , by a completely different approach (although it uses infxpen via xpomen ). Using Cantor's normal form, we can show that A ^o B respects equinumerosity ( oef1o ), so that all the steps of (om ^ W ) x. ( om ^ W ) ~_om ^ ( 2 W ) ~ (om ^ 2 ) ^ W ~_om ^ W can be verified using bijections to do the ordinal commutations. (The assumption on N can be satisfied using cnfcom3c .) (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

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

Proof

Step Hyp Ref Expression
1 infxpenc.1 
 |-  ( ph -> A e. On )
2 infxpenc.2 
 |-  ( ph -> _om C_ A )
3 infxpenc.3 
 |-  ( ph -> W e. ( On \ 1o ) )
4 infxpenc.4 
 |-  ( ph -> F : ( _om ^o 2o ) -1-1-onto-> _om )
5 infxpenc.5 
 |-  ( ph -> ( F ` (/) ) = (/) )
6 infxpenc.6 
 |-  ( ph -> N : A -1-1-onto-> ( _om ^o W ) )
7 infxpenc.k 
 |-  K = ( y e. { x e. ( ( _om ^o 2o ) ^m W ) | x finSupp (/) } |-> ( F o. ( y o. `' ( _I |` W ) ) ) )
8 infxpenc.h 
 |-  H = ( ( ( _om CNF W ) o. K ) o. `' ( ( _om ^o 2o ) CNF W ) )
9 infxpenc.l 
 |-  L = ( y e. { x e. ( _om ^m ( W .o 2o ) ) | x finSupp (/) } |-> ( ( _I |` _om ) o. ( y o. `' ( Y o. `' X ) ) ) )
10 infxpenc.x 
 |-  X = ( z e. 2o , w e. W |-> ( ( W .o z ) +o w ) )
11 infxpenc.y 
 |-  Y = ( z e. 2o , w e. W |-> ( ( 2o .o w ) +o z ) )
12 infxpenc.j 
 |-  J = ( ( ( _om CNF ( 2o .o W ) ) o. L ) o. `' ( _om CNF ( W .o 2o ) ) )
13 infxpenc.z 
 |-  Z = ( x e. ( _om ^o W ) , y e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o x ) +o y ) )
14 infxpenc.t 
 |-  T = ( x e. A , y e. A |-> <. ( N ` x ) , ( N ` y ) >. )
15 infxpenc.g 
 |-  G = ( `' N o. ( ( ( H o. J ) o. Z ) o. T ) )
16 f1ocnv 
 |-  ( N : A -1-1-onto-> ( _om ^o W ) -> `' N : ( _om ^o W ) -1-1-onto-> A )
17 6 16 syl 
 |-  ( ph -> `' N : ( _om ^o W ) -1-1-onto-> A )
18 f1oi 
 |-  ( _I |` W ) : W -1-1-onto-> W
19 18 a1i 
 |-  ( ph -> ( _I |` W ) : W -1-1-onto-> W )
20 omelon 
 |-  _om e. On
21 20 a1i 
 |-  ( ph -> _om e. On )
22 2on 
 |-  2o e. On
23 oecl 
 |-  ( ( _om e. On /\ 2o e. On ) -> ( _om ^o 2o ) e. On )
24 21 22 23 sylancl 
 |-  ( ph -> ( _om ^o 2o ) e. On )
25 22 a1i 
 |-  ( ph -> 2o e. On )
26 peano1 
 |-  (/) e. _om
27 26 a1i 
 |-  ( ph -> (/) e. _om )
28 oen0 
 |-  ( ( ( _om e. On /\ 2o e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o 2o ) )
29 21 25 27 28 syl21anc 
 |-  ( ph -> (/) e. ( _om ^o 2o ) )
30 ondif1 
 |-  ( ( _om ^o 2o ) e. ( On \ 1o ) <-> ( ( _om ^o 2o ) e. On /\ (/) e. ( _om ^o 2o ) ) )
31 24 29 30 sylanbrc 
 |-  ( ph -> ( _om ^o 2o ) e. ( On \ 1o ) )
32 3 eldifad 
 |-  ( ph -> W e. On )
33 4 19 31 32 21 32 5 7 8 oef1o 
 |-  ( ph -> H : ( ( _om ^o 2o ) ^o W ) -1-1-onto-> ( _om ^o W ) )
34 f1oi 
 |-  ( _I |` _om ) : _om -1-1-onto-> _om
35 34 a1i 
 |-  ( ph -> ( _I |` _om ) : _om -1-1-onto-> _om )
36 10 11 omf1o 
 |-  ( ( W e. On /\ 2o e. On ) -> ( Y o. `' X ) : ( W .o 2o ) -1-1-onto-> ( 2o .o W ) )
37 32 22 36 sylancl 
 |-  ( ph -> ( Y o. `' X ) : ( W .o 2o ) -1-1-onto-> ( 2o .o W ) )
38 ondif1 
 |-  ( _om e. ( On \ 1o ) <-> ( _om e. On /\ (/) e. _om ) )
39 20 26 38 mpbir2an 
 |-  _om e. ( On \ 1o )
40 39 a1i 
 |-  ( ph -> _om e. ( On \ 1o ) )
41 omcl 
 |-  ( ( W e. On /\ 2o e. On ) -> ( W .o 2o ) e. On )
42 32 22 41 sylancl 
 |-  ( ph -> ( W .o 2o ) e. On )
43 omcl 
 |-  ( ( 2o e. On /\ W e. On ) -> ( 2o .o W ) e. On )
44 25 32 43 syl2anc 
 |-  ( ph -> ( 2o .o W ) e. On )
45 fvresi 
 |-  ( (/) e. _om -> ( ( _I |` _om ) ` (/) ) = (/) )
46 26 45 mp1i 
 |-  ( ph -> ( ( _I |` _om ) ` (/) ) = (/) )
47 35 37 40 42 21 44 46 9 12 oef1o 
 |-  ( ph -> J : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( _om ^o ( 2o .o W ) ) )
48 oeoe 
 |-  ( ( _om e. On /\ 2o e. On /\ W e. On ) -> ( ( _om ^o 2o ) ^o W ) = ( _om ^o ( 2o .o W ) ) )
49 20 25 32 48 mp3an2i 
 |-  ( ph -> ( ( _om ^o 2o ) ^o W ) = ( _om ^o ( 2o .o W ) ) )
50 49 f1oeq3d 
 |-  ( ph -> ( J : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( ( _om ^o 2o ) ^o W ) <-> J : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( _om ^o ( 2o .o W ) ) ) )
51 47 50 mpbird 
 |-  ( ph -> J : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( ( _om ^o 2o ) ^o W ) )
52 f1oco 
 |-  ( ( H : ( ( _om ^o 2o ) ^o W ) -1-1-onto-> ( _om ^o W ) /\ J : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( ( _om ^o 2o ) ^o W ) ) -> ( H o. J ) : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( _om ^o W ) )
53 33 51 52 syl2anc 
 |-  ( ph -> ( H o. J ) : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( _om ^o W ) )
54 df-2o 
 |-  2o = suc 1o
55 54 oveq2i 
 |-  ( W .o 2o ) = ( W .o suc 1o )
56 1on 
 |-  1o e. On
57 omsuc 
 |-  ( ( W e. On /\ 1o e. On ) -> ( W .o suc 1o ) = ( ( W .o 1o ) +o W ) )
58 32 56 57 sylancl 
 |-  ( ph -> ( W .o suc 1o ) = ( ( W .o 1o ) +o W ) )
59 55 58 syl5eq 
 |-  ( ph -> ( W .o 2o ) = ( ( W .o 1o ) +o W ) )
60 om1 
 |-  ( W e. On -> ( W .o 1o ) = W )
61 32 60 syl 
 |-  ( ph -> ( W .o 1o ) = W )
62 61 oveq1d 
 |-  ( ph -> ( ( W .o 1o ) +o W ) = ( W +o W ) )
63 59 62 eqtrd 
 |-  ( ph -> ( W .o 2o ) = ( W +o W ) )
64 63 oveq2d 
 |-  ( ph -> ( _om ^o ( W .o 2o ) ) = ( _om ^o ( W +o W ) ) )
65 oeoa 
 |-  ( ( _om e. On /\ W e. On /\ W e. On ) -> ( _om ^o ( W +o W ) ) = ( ( _om ^o W ) .o ( _om ^o W ) ) )
66 20 32 32 65 mp3an2i 
 |-  ( ph -> ( _om ^o ( W +o W ) ) = ( ( _om ^o W ) .o ( _om ^o W ) ) )
67 64 66 eqtrd 
 |-  ( ph -> ( _om ^o ( W .o 2o ) ) = ( ( _om ^o W ) .o ( _om ^o W ) ) )
68 67 f1oeq2d 
 |-  ( ph -> ( ( H o. J ) : ( _om ^o ( W .o 2o ) ) -1-1-onto-> ( _om ^o W ) <-> ( H o. J ) : ( ( _om ^o W ) .o ( _om ^o W ) ) -1-1-onto-> ( _om ^o W ) ) )
69 53 68 mpbid 
 |-  ( ph -> ( H o. J ) : ( ( _om ^o W ) .o ( _om ^o W ) ) -1-1-onto-> ( _om ^o W ) )
70 oecl 
 |-  ( ( _om e. On /\ W e. On ) -> ( _om ^o W ) e. On )
71 21 32 70 syl2anc 
 |-  ( ph -> ( _om ^o W ) e. On )
72 13 omxpenlem 
 |-  ( ( ( _om ^o W ) e. On /\ ( _om ^o W ) e. On ) -> Z : ( ( _om ^o W ) X. ( _om ^o W ) ) -1-1-onto-> ( ( _om ^o W ) .o ( _om ^o W ) ) )
73 71 71 72 syl2anc 
 |-  ( ph -> Z : ( ( _om ^o W ) X. ( _om ^o W ) ) -1-1-onto-> ( ( _om ^o W ) .o ( _om ^o W ) ) )
74 f1oco 
 |-  ( ( ( H o. J ) : ( ( _om ^o W ) .o ( _om ^o W ) ) -1-1-onto-> ( _om ^o W ) /\ Z : ( ( _om ^o W ) X. ( _om ^o W ) ) -1-1-onto-> ( ( _om ^o W ) .o ( _om ^o W ) ) ) -> ( ( H o. J ) o. Z ) : ( ( _om ^o W ) X. ( _om ^o W ) ) -1-1-onto-> ( _om ^o W ) )
75 69 73 74 syl2anc 
 |-  ( ph -> ( ( H o. J ) o. Z ) : ( ( _om ^o W ) X. ( _om ^o W ) ) -1-1-onto-> ( _om ^o W ) )
76 f1of 
 |-  ( N : A -1-1-onto-> ( _om ^o W ) -> N : A --> ( _om ^o W ) )
77 6 76 syl 
 |-  ( ph -> N : A --> ( _om ^o W ) )
78 77 feqmptd 
 |-  ( ph -> N = ( x e. A |-> ( N ` x ) ) )
79 f1oeq1 
 |-  ( N = ( x e. A |-> ( N ` x ) ) -> ( N : A -1-1-onto-> ( _om ^o W ) <-> ( x e. A |-> ( N ` x ) ) : A -1-1-onto-> ( _om ^o W ) ) )
80 78 79 syl 
 |-  ( ph -> ( N : A -1-1-onto-> ( _om ^o W ) <-> ( x e. A |-> ( N ` x ) ) : A -1-1-onto-> ( _om ^o W ) ) )
81 6 80 mpbid 
 |-  ( ph -> ( x e. A |-> ( N ` x ) ) : A -1-1-onto-> ( _om ^o W ) )
82 77 feqmptd 
 |-  ( ph -> N = ( y e. A |-> ( N ` y ) ) )
83 f1oeq1 
 |-  ( N = ( y e. A |-> ( N ` y ) ) -> ( N : A -1-1-onto-> ( _om ^o W ) <-> ( y e. A |-> ( N ` y ) ) : A -1-1-onto-> ( _om ^o W ) ) )
84 82 83 syl 
 |-  ( ph -> ( N : A -1-1-onto-> ( _om ^o W ) <-> ( y e. A |-> ( N ` y ) ) : A -1-1-onto-> ( _om ^o W ) ) )
85 6 84 mpbid 
 |-  ( ph -> ( y e. A |-> ( N ` y ) ) : A -1-1-onto-> ( _om ^o W ) )
86 81 85 xpf1o 
 |-  ( ph -> ( x e. A , y e. A |-> <. ( N ` x ) , ( N ` y ) >. ) : ( A X. A ) -1-1-onto-> ( ( _om ^o W ) X. ( _om ^o W ) ) )
87 f1oeq1 
 |-  ( T = ( x e. A , y e. A |-> <. ( N ` x ) , ( N ` y ) >. ) -> ( T : ( A X. A ) -1-1-onto-> ( ( _om ^o W ) X. ( _om ^o W ) ) <-> ( x e. A , y e. A |-> <. ( N ` x ) , ( N ` y ) >. ) : ( A X. A ) -1-1-onto-> ( ( _om ^o W ) X. ( _om ^o W ) ) ) )
88 14 87 ax-mp 
 |-  ( T : ( A X. A ) -1-1-onto-> ( ( _om ^o W ) X. ( _om ^o W ) ) <-> ( x e. A , y e. A |-> <. ( N ` x ) , ( N ` y ) >. ) : ( A X. A ) -1-1-onto-> ( ( _om ^o W ) X. ( _om ^o W ) ) )
89 86 88 sylibr 
 |-  ( ph -> T : ( A X. A ) -1-1-onto-> ( ( _om ^o W ) X. ( _om ^o W ) ) )
90 f1oco 
 |-  ( ( ( ( H o. J ) o. Z ) : ( ( _om ^o W ) X. ( _om ^o W ) ) -1-1-onto-> ( _om ^o W ) /\ T : ( A X. A ) -1-1-onto-> ( ( _om ^o W ) X. ( _om ^o W ) ) ) -> ( ( ( H o. J ) o. Z ) o. T ) : ( A X. A ) -1-1-onto-> ( _om ^o W ) )
91 75 89 90 syl2anc 
 |-  ( ph -> ( ( ( H o. J ) o. Z ) o. T ) : ( A X. A ) -1-1-onto-> ( _om ^o W ) )
92 f1oco 
 |-  ( ( `' N : ( _om ^o W ) -1-1-onto-> A /\ ( ( ( H o. J ) o. Z ) o. T ) : ( A X. A ) -1-1-onto-> ( _om ^o W ) ) -> ( `' N o. ( ( ( H o. J ) o. Z ) o. T ) ) : ( A X. A ) -1-1-onto-> A )
93 17 91 92 syl2anc 
 |-  ( ph -> ( `' N o. ( ( ( H o. J ) o. Z ) o. T ) ) : ( A X. A ) -1-1-onto-> A )
94 f1oeq1 
 |-  ( G = ( `' N o. ( ( ( H o. J ) o. Z ) o. T ) ) -> ( G : ( A X. A ) -1-1-onto-> A <-> ( `' N o. ( ( ( H o. J ) o. Z ) o. T ) ) : ( A X. A ) -1-1-onto-> A ) )
95 15 94 ax-mp 
 |-  ( G : ( A X. A ) -1-1-onto-> A <-> ( `' N o. ( ( ( H o. J ) o. Z ) o. T ) ) : ( A X. A ) -1-1-onto-> A )
96 93 95 sylibr 
 |-  ( ph -> G : ( A X. A ) -1-1-onto-> A )