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 27 f1oeq1d 
 |-  ( 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 ) ) ) )
29 26 28 mpbird 
 |-  ( ph -> ( T ` dom G ) : ( H ` suc U. dom G ) -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) )
30 omelon 
 |-  _om e. On
31 30 a1i 
 |-  ( ph -> _om e. On )
32 1 31 2 cantnff1o 
 |-  ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) )
33 f1ocnv 
 |-  ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S )
34 f1of 
 |-  ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
35 32 33 34 3syl 
 |-  ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
36 35 3 ffvelrnd 
 |-  ( ph -> ( `' ( _om CNF A ) ` B ) e. S )
37 4 36 eqeltrid 
 |-  ( ph -> F e. S )
38 8 oveq1i 
 |-  ( M +o z ) = ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z )
39 38 a1i 
 |-  ( ( k e. _V /\ z e. _V ) -> ( M +o z ) = ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) )
40 39 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 ) )
41 eqid 
 |-  (/) = (/)
42 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 ) ) , (/) ) )
43 40 41 42 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 ) ) , (/) )
44 6 43 eqtri 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
45 1 31 2 5 37 44 cantnfval 
 |-  ( ph -> ( ( _om CNF A ) ` F ) = ( H ` dom G ) )
46 4 fveq2i 
 |-  ( ( _om CNF A ) ` F ) = ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) )
47 45 46 eqtr3di 
 |-  ( ph -> ( H ` dom G ) = ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) )
48 18 fveq2d 
 |-  ( ph -> ( H ` dom G ) = ( H ` suc U. dom G ) )
49 f1ocnvfv2 
 |-  ( ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) /\ B e. ( _om ^o A ) ) -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
50 32 3 49 syl2anc 
 |-  ( ph -> ( ( _om CNF A ) ` ( `' ( _om CNF A ) ` B ) ) = B )
51 47 48 50 3eqtr3d 
 |-  ( ph -> ( H ` suc U. dom G ) = B )
52 51 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 ) ) ) )
53 29 52 mpbid 
 |-  ( ph -> ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) )