Metamath Proof Explorer

Theorem cnfcom3

Description: Any infinite ordinal B is equinumerous to a power of _om . (We are being careful here to show explicit bijections rather than simple equinumerosity because we want a uniform construction for cnfcom3c .) (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 4-Jul-2019)

Ref Expression
Hypotheses cnfcom.s 
|- S = dom ( _om CNF A )
cnfcom.a 
|- ( ph -> A e. On )
cnfcom.b 
|- ( ph -> B e. ( _om ^o A ) )
cnfcom.f 
|- F = ( `' ( _om CNF A ) ` B )
cnfcom.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cnfcom.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
cnfcom.t 
|- T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
cnfcom.m 
|- M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
cnfcom.k 
|- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
cnfcom.w 
|- W = ( G ` U. dom G )
cnfcom3.1 
|- ( ph -> _om C_ B )
cnfcom.x 
|- X = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) )
cnfcom.y 
|- Y = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o u ) +o v ) )
cnfcom.n 
|- N = ( ( X o. `' Y ) o. ( T ` dom G ) )
Assertion cnfcom3 
|- ( ph -> N : B -1-1-onto-> ( _om ^o W ) )

Proof

Step Hyp Ref Expression
1 cnfcom.s 
 |-  S = dom ( _om CNF A )
2 cnfcom.a 
 |-  ( ph -> A e. On )
3 cnfcom.b 
 |-  ( ph -> B e. ( _om ^o A ) )
4 cnfcom.f 
 |-  F = ( `' ( _om CNF A ) ` B )
5 cnfcom.g 
 |-  G = OrdIso ( _E , ( F supp (/) ) )
6 cnfcom.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) )
7 cnfcom.t 
 |-  T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) )
8 cnfcom.m 
 |-  M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) )
9 cnfcom.k 
 |-  K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) )
10 cnfcom.w 
 |-  W = ( G ` U. dom G )
11 cnfcom3.1 
 |-  ( ph -> _om C_ B )
12 cnfcom.x 
 |-  X = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) )
13 cnfcom.y 
 |-  Y = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o u ) +o v ) )
14 cnfcom.n 
 |-  N = ( ( X o. `' Y ) o. ( T ` dom G ) )
15 omelon 
 |-  _om e. On
16 suppssdm 
 |-  ( F supp (/) ) C_ dom F
17 15 a1i 
 |-  ( ph -> _om e. On )
18 1 17 2 cantnff1o 
 |-  ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) )
19 f1ocnv 
 |-  ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S )
20 f1of 
 |-  ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
21 18 19 20 3syl 
 |-  ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
22 21 3 ffvelcdmd 
 |-  ( ph -> ( `' ( _om CNF A ) ` B ) e. S )
23 4 22 eqeltrid 
 |-  ( ph -> F e. S )
24 1 17 2 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : A --> _om /\ F finSupp (/) ) ) )
25 23 24 mpbid 
 |-  ( ph -> ( F : A --> _om /\ F finSupp (/) ) )
26 25 simpld 
 |-  ( ph -> F : A --> _om )
27 16 26 fssdm 
 |-  ( ph -> ( F supp (/) ) C_ A )
28 ovex 
 |-  ( F supp (/) ) e. _V
29 5 oion 
 |-  ( ( F supp (/) ) e. _V -> dom G e. On )
30 28 29 ax-mp 
 |-  dom G e. On
31 30 elexi 
 |-  dom G e. _V
32 31 uniex 
 |-  U. dom G e. _V
33 32 sucid 
 |-  U. dom G e. suc U. dom G
34 peano1 
 |-  (/) e. _om
35 34 a1i 
 |-  ( ph -> (/) e. _om )
36 11 35 sseldd 
 |-  ( ph -> (/) e. B )
37 1 2 3 4 5 6 7 8 9 10 36 cnfcom2lem 
 |-  ( ph -> dom G = suc U. dom G )
38 33 37 eleqtrrid 
 |-  ( ph -> U. dom G e. dom G )
39 5 oif 
 |-  G : dom G --> ( F supp (/) )
40 39 ffvelcdmi 
 |-  ( U. dom G e. dom G -> ( G ` U. dom G ) e. ( F supp (/) ) )
41 38 40 syl 
 |-  ( ph -> ( G ` U. dom G ) e. ( F supp (/) ) )
42 10 41 eqeltrid 
 |-  ( ph -> W e. ( F supp (/) ) )
43 27 42 sseldd 
 |-  ( ph -> W e. A )
44 onelon 
 |-  ( ( A e. On /\ W e. A ) -> W e. On )
45 2 43 44 syl2anc 
 |-  ( ph -> W e. On )
46 oecl 
 |-  ( ( _om e. On /\ W e. On ) -> ( _om ^o W ) e. On )
47 15 45 46 sylancr 
 |-  ( ph -> ( _om ^o W ) e. On )
48 26 43 ffvelcdmd 
 |-  ( ph -> ( F ` W ) e. _om )
49 nnon 
 |-  ( ( F ` W ) e. _om -> ( F ` W ) e. On )
50 48 49 syl 
 |-  ( ph -> ( F ` W ) e. On )
51 13 12 omf1o 
 |-  ( ( ( _om ^o W ) e. On /\ ( F ` W ) e. On ) -> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( ( F ` W ) .o ( _om ^o W ) ) )
52 47 50 51 syl2anc 
 |-  ( ph -> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( ( F ` W ) .o ( _om ^o W ) ) )
53 26 ffnd 
 |-  ( ph -> F Fn A )
54 0ex 
 |-  (/) e. _V
55 54 a1i 
 |-  ( ph -> (/) e. _V )
56 elsuppfn 
 |-  ( ( F Fn A /\ A e. On /\ (/) e. _V ) -> ( W e. ( F supp (/) ) <-> ( W e. A /\ ( F ` W ) =/= (/) ) ) )
57 53 2 55 56 syl3anc 
 |-  ( ph -> ( W e. ( F supp (/) ) <-> ( W e. A /\ ( F ` W ) =/= (/) ) ) )
58 simpr 
 |-  ( ( W e. A /\ ( F ` W ) =/= (/) ) -> ( F ` W ) =/= (/) )
59 57 58 biimtrdi 
 |-  ( ph -> ( W e. ( F supp (/) ) -> ( F ` W ) =/= (/) ) )
60 42 59 mpd 
 |-  ( ph -> ( F ` W ) =/= (/) )
61 on0eln0 
 |-  ( ( F ` W ) e. On -> ( (/) e. ( F ` W ) <-> ( F ` W ) =/= (/) ) )
62 48 49 61 3syl 
 |-  ( ph -> ( (/) e. ( F ` W ) <-> ( F ` W ) =/= (/) ) )
63 60 62 mpbird 
 |-  ( ph -> (/) e. ( F ` W ) )
64 1 2 3 4 5 6 7 8 9 10 11 cnfcom3lem 
 |-  ( ph -> W e. ( On \ 1o ) )
65 ondif1 
 |-  ( W e. ( On \ 1o ) <-> ( W e. On /\ (/) e. W ) )
66 65 simprbi 
 |-  ( W e. ( On \ 1o ) -> (/) e. W )
67 64 66 syl 
 |-  ( ph -> (/) e. W )
68 omabs 
 |-  ( ( ( ( F ` W ) e. _om /\ (/) e. ( F ` W ) ) /\ ( W e. On /\ (/) e. W ) ) -> ( ( F ` W ) .o ( _om ^o W ) ) = ( _om ^o W ) )
69 48 63 45 67 68 syl22anc 
 |-  ( ph -> ( ( F ` W ) .o ( _om ^o W ) ) = ( _om ^o W ) )
70 69 f1oeq3d 
 |-  ( ph -> ( ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( ( F ` W ) .o ( _om ^o W ) ) <-> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( _om ^o W ) ) )
71 52 70 mpbid 
 |-  ( ph -> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( _om ^o W ) )
72 1 2 3 4 5 6 7 8 9 10 36 cnfcom2 
 |-  ( ph -> ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) )
73 f1oco 
 |-  ( ( ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( _om ^o W ) /\ ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) ) -> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) )
74 71 72 73 syl2anc 
 |-  ( ph -> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) )
75 f1oeq1 
 |-  ( N = ( ( X o. `' Y ) o. ( T ` dom G ) ) -> ( N : B -1-1-onto-> ( _om ^o W ) <-> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) ) )
76 14 75 ax-mp 
 |-  ( N : B -1-1-onto-> ( _om ^o W ) <-> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) )
77 74 76 sylibr 
 |-  ( ph -> N : B -1-1-onto-> ( _om ^o W ) )