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 ffvelrnd
 |-  ( 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 ffvelrni
 |-  ( 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 ffvelrnd
 |-  ( 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 syl6bi
 |-  ( 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 ) )