Metamath Proof Explorer

Theorem cnfcom2

Description: Any nonzero ordinal B is equinumerous to the leading term of its Cantor normal form. (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-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 )
cnfcom2.1 
|- ( ph -> (/) e. B )
Assertion cnfcom2 
|- ( ph -> ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` 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 cnfcom2.1 
 |-  ( ph -> (/) e. B )
12 ovex 
 |-  ( F supp (/) ) e. _V
13 5 oion 
 |-  ( ( F supp (/) ) e. _V -> dom G e. On )
14 12 13 ax-mp 
 |-  dom G e. On
15 14 elexi 
 |-  dom G e. _V
16 15 uniex 
 |-  U. dom G e. _V
17 16 sucid 
 |-  U. dom G e. suc U. dom G
18 1 2 3 4 5 6 7 8 9 10 11 cnfcom2lem 
 |-  ( ph -> dom G = suc U. dom G )
19 17 18 eleqtrrid 
 |-  ( ph -> U. dom G e. dom G )
20 1 2 3 4 5 6 7 8 9 19 cnfcom 
 |-  ( ph -> ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o ( G ` U. dom G ) ) .o ( F ` ( G ` U. dom G ) ) ) )
21 10 oveq2i 
 |-  ( _om ^o W ) = ( _om ^o ( G ` U. dom G ) )
22 10 fveq2i 
 |-  ( F ` W ) = ( F ` ( G ` U. dom G ) )
23 21 22 oveq12i 
 |-  ( ( _om ^o W ) .o ( F ` W ) ) = ( ( _om ^o ( G ` U. dom G ) ) .o ( F ` ( G ` U. dom G ) ) )
24 f1oeq3 
 |-  ( ( ( _om ^o W ) .o ( F ` W ) ) = ( ( _om ^o ( G ` U. dom G ) ) .o ( F ` ( G ` U. dom G ) ) ) -> ( ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) <-> ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o ( G ` U. dom G ) ) .o ( F ` ( G ` U. dom G ) ) ) ) )
25 23 24 ax-mp 
 |-  ( ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) <-> ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o ( G ` U. dom G ) ) .o ( F ` ( G ` U. dom G ) ) ) )
26 20 25 sylibr 
 |-  ( ph -> ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) )
27 18 fveq2d 
 |-  ( ph -> ( T ` dom G ) = ( T ` suc U. dom G ) )
28 f1oeq1 
 |-  ( ( T ` dom G ) = ( T ` suc U. dom G ) -> ( ( T ` dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) <-> ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) ) )
29 27 28 syl 
 |-  ( ph -> ( ( T ` dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) <-> ( T ` suc U. dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) ) )
30 26 29 mpbird 
 |-  ( ph -> ( T ` dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) )
31 4 fveq2i 
 |-  ( ( _om CNF A ) ` F ) = ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) )
32 omelon 
 |-  _om e. On
33 32 a1i 
 |-  ( ph -> _om e. On )
34 1 33 2 cantnff1o 
 |-  ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) )
35 f1ocnv 
 |-  ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S )
36 f1of 
 |-  ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
37 34 35 36 3syl 
 |-  ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
38 37 3 ffvelrnd 
 |-  ( ph -> ( `' ( _om CNF A ) ` B ) e. S )
39 4 38 eqeltrid 
 |-  ( ph -> F e. S )
40 8 oveq1i 
 |-  ( M +o z ) = ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z )
41 40 a1i 
 |-  ( ( k e. _V /\ z e. _V ) -> ( M +o z ) = ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) )
42 41 mpoeq3ia 
 |-  ( k e. _V , z e. _V |-> ( M +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) )
43 eqid 
 |-  (/) = (/)
44 seqomeq12 
 |-  ( ( ( k e. _V , z e. _V |-> ( M +o z ) ) = ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) /\ (/) = (/) ) -> seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) ) )
45 42 43 44 mp2an 
 |-  seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
46 6 45 eqtri 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
47 1 33 2 5 39 46 cantnfval 
 |-  ( ph -> ( ( _om CNF A ) ` F ) = ( H ` dom G ) )
48 31 47 syl5reqr 
 |-  ( ph -> ( H ` dom G ) = ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) )
49 18 fveq2d 
 |-  ( ph -> ( H ` dom G ) = ( H ` suc U. dom G ) )
50 f1ocnvfv2 
 |-  ( ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) /\ B e. ( _om ^o A ) ) -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
51 34 3 50 syl2anc 
 |-  ( ph -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
52 48 49 51 3eqtr3d 
 |-  ( ph -> ( H ` suc U. dom G ) = B )
53 52 f1oeq2d 
 |-  ( ph -> ( ( T ` dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) <-> ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) ) )
54 30 53 mpbid 
 |-  ( ph -> ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) )