Metamath Proof Explorer

Theorem cnfcom

Description: Any ordinal B is equinumerous to the leading term of its Cantor normal form. Here we show that bijection explicitly. (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.1 
|- ( ph -> I e. dom G )
Assertion cnfcom 
|- ( ph -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )

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.1 
 |-  ( ph -> I e. dom G )
11 omelon 
 |-  _om e. On
12 11 a1i 
 |-  ( ph -> _om e. On )
13 1 12 2 cantnff1o 
 |-  ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) )
14 f1ocnv 
 |-  ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S )
15 f1of 
 |-  ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
16 13 14 15 3syl 
 |-  ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S )
17 16 3 ffvelrnd 
 |-  ( ph -> ( `' ( _om CNF A ) ` B ) e. S )
18 4 17 eqeltrid 
 |-  ( ph -> F e. S )
19 1 12 2 5 18 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )
20 19 simprd 
 |-  ( ph -> dom G e. _om )
21 elnn 
 |-  ( ( I e. dom G /\ dom G e. _om ) -> I e. _om )
22 10 20 21 syl2anc 
 |-  ( ph -> I e. _om )
23 eleq1 
 |-  ( w = I -> ( w e. dom G <-> I e. dom G ) )
24 suceq 
 |-  ( w = I -> suc w = suc I )
25 24 fveq2d 
 |-  ( w = I -> ( T ` suc w ) = ( T ` suc I ) )
26 24 fveq2d 
 |-  ( w = I -> ( H ` suc w ) = ( H ` suc I ) )
27 fveq2 
 |-  ( w = I -> ( G ` w ) = ( G ` I ) )
28 27 oveq2d 
 |-  ( w = I -> ( _om ^o ( G ` w ) ) = ( _om ^o ( G ` I ) ) )
29 2fveq3 
 |-  ( w = I -> ( F ` ( G ` w ) ) = ( F ` ( G ` I ) ) )
30 28 29 oveq12d 
 |-  ( w = I -> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) = ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )
31 25 26 30 f1oeq123d 
 |-  ( w = I -> ( ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) <-> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) )
32 23 31 imbi12d 
 |-  ( w = I -> ( ( w e. dom G -> ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) ) <-> ( I e. dom G -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) ) )
33 32 imbi2d 
 |-  ( w = I -> ( ( ph -> ( w e. dom G -> ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) ) ) <-> ( ph -> ( I e. dom G -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) ) ) )
34 eleq1 
 |-  ( w = (/) -> ( w e. dom G <-> (/) e. dom G ) )
35 suceq 
 |-  ( w = (/) -> suc w = suc (/) )
36 35 fveq2d 
 |-  ( w = (/) -> ( T ` suc w ) = ( T ` suc (/) ) )
37 35 fveq2d 
 |-  ( w = (/) -> ( H ` suc w ) = ( H ` suc (/) ) )
38 fveq2 
 |-  ( w = (/) -> ( G ` w ) = ( G ` (/) ) )
39 38 oveq2d 
 |-  ( w = (/) -> ( _om ^o ( G ` w ) ) = ( _om ^o ( G ` (/) ) ) )
40 2fveq3 
 |-  ( w = (/) -> ( F ` ( G ` w ) ) = ( F ` ( G ` (/) ) ) )
41 39 40 oveq12d 
 |-  ( w = (/) -> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) = ( ( _om ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) )
42 36 37 41 f1oeq123d 
 |-  ( w = (/) -> ( ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) <-> ( T ` suc (/) ) : ( H ` suc (/) ) -1-1-onto-> ( ( _om ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) ) )
43 34 42 imbi12d 
 |-  ( w = (/) -> ( ( w e. dom G -> ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) ) <-> ( (/) e. dom G -> ( T ` suc (/) ) : ( H ` suc (/) ) -1-1-onto-> ( ( _om ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) ) ) )
44 eleq1 
 |-  ( w = y -> ( w e. dom G <-> y e. dom G ) )
45 suceq 
 |-  ( w = y -> suc w = suc y )
46 45 fveq2d 
 |-  ( w = y -> ( T ` suc w ) = ( T ` suc y ) )
47 45 fveq2d 
 |-  ( w = y -> ( H ` suc w ) = ( H ` suc y ) )
48 fveq2 
 |-  ( w = y -> ( G ` w ) = ( G ` y ) )
49 48 oveq2d 
 |-  ( w = y -> ( _om ^o ( G ` w ) ) = ( _om ^o ( G ` y ) ) )
50 2fveq3 
 |-  ( w = y -> ( F ` ( G ` w ) ) = ( F ` ( G ` y ) ) )
51 49 50 oveq12d 
 |-  ( w = y -> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) = ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) )
52 46 47 51 f1oeq123d 
 |-  ( w = y -> ( ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) <-> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) )
53 44 52 imbi12d 
 |-  ( w = y -> ( ( w e. dom G -> ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) ) <-> ( y e. dom G -> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) )
54 eleq1 
 |-  ( w = suc y -> ( w e. dom G <-> suc y e. dom G ) )
55 suceq 
 |-  ( w = suc y -> suc w = suc suc y )
56 55 fveq2d 
 |-  ( w = suc y -> ( T ` suc w ) = ( T ` suc suc y ) )
57 55 fveq2d 
 |-  ( w = suc y -> ( H ` suc w ) = ( H ` suc suc y ) )
58 fveq2 
 |-  ( w = suc y -> ( G ` w ) = ( G ` suc y ) )
59 58 oveq2d 
 |-  ( w = suc y -> ( _om ^o ( G ` w ) ) = ( _om ^o ( G ` suc y ) ) )
60 2fveq3 
 |-  ( w = suc y -> ( F ` ( G ` w ) ) = ( F ` ( G ` suc y ) ) )
61 59 60 oveq12d 
 |-  ( w = suc y -> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) = ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) )
62 56 57 61 f1oeq123d 
 |-  ( w = suc y -> ( ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) <-> ( T ` suc suc y ) : ( H ` suc suc y ) -1-1-onto-> ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) ) )
63 54 62 imbi12d 
 |-  ( w = suc y -> ( ( w e. dom G -> ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) ) <-> ( suc y e. dom G -> ( T ` suc suc y ) : ( H ` suc suc y ) -1-1-onto-> ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) ) ) )
64 2 adantr 
 |-  ( ( ph /\ (/) e. dom G ) -> A e. On )
65 3 adantr 
 |-  ( ( ph /\ (/) e. dom G ) -> B e. ( _om ^o A ) )
66 simpr 
 |-  ( ( ph /\ (/) e. dom G ) -> (/) e. dom G )
67 11 a1i 
 |-  ( ( ph /\ (/) e. dom G ) -> _om e. On )
68 suppssdm 
 |-  ( F supp (/) ) C_ dom F
69 1 12 2 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : A --> _om /\ F finSupp (/) ) ) )
70 18 69 mpbid 
 |-  ( ph -> ( F : A --> _om /\ F finSupp (/) ) )
71 70 simpld 
 |-  ( ph -> F : A --> _om )
72 68 71 fssdm 
 |-  ( ph -> ( F supp (/) ) C_ A )
73 onss 
 |-  ( A e. On -> A C_ On )
74 2 73 syl 
 |-  ( ph -> A C_ On )
75 72 74 sstrd 
 |-  ( ph -> ( F supp (/) ) C_ On )
76 5 oif 
 |-  G : dom G --> ( F supp (/) )
77 76 ffvelrni 
 |-  ( (/) e. dom G -> ( G ` (/) ) e. ( F supp (/) ) )
78 ssel2 
 |-  ( ( ( F supp (/) ) C_ On /\ ( G ` (/) ) e. ( F supp (/) ) ) -> ( G ` (/) ) e. On )
79 75 77 78 syl2an 
 |-  ( ( ph /\ (/) e. dom G ) -> ( G ` (/) ) e. On )
80 peano1 
 |-  (/) e. _om
81 80 a1i 
 |-  ( ( ph /\ (/) e. dom G ) -> (/) e. _om )
82 oen0 
 |-  ( ( ( _om e. On /\ ( G ` (/) ) e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o ( G ` (/) ) ) )
83 67 79 81 82 syl21anc 
 |-  ( ( ph /\ (/) e. dom G ) -> (/) e. ( _om ^o ( G ` (/) ) ) )
84 0ex 
 |-  (/) e. _V
85 7 seqom0g 
 |-  ( (/) e. _V -> ( T ` (/) ) = (/) )
86 84 85 ax-mp 
 |-  ( T ` (/) ) = (/)
87 f1o0 
 |-  (/) : (/) -1-1-onto-> (/)
88 6 seqom0g 
 |-  ( (/) e. _V -> ( H ` (/) ) = (/) )
89 f1oeq2 
 |-  ( ( H ` (/) ) = (/) -> ( (/) : ( H ` (/) ) -1-1-onto-> (/) <-> (/) : (/) -1-1-onto-> (/) ) )
90 84 88 89 mp2b 
 |-  ( (/) : ( H ` (/) ) -1-1-onto-> (/) <-> (/) : (/) -1-1-onto-> (/) )
91 87 90 mpbir 
 |-  (/) : ( H ` (/) ) -1-1-onto-> (/)
92 f1oeq1 
 |-  ( ( T ` (/) ) = (/) -> ( ( T ` (/) ) : ( H ` (/) ) -1-1-onto-> (/) <-> (/) : ( H ` (/) ) -1-1-onto-> (/) ) )
93 91 92 mpbiri 
 |-  ( ( T ` (/) ) = (/) -> ( T ` (/) ) : ( H ` (/) ) -1-1-onto-> (/) )
94 86 93 mp1i 
 |-  ( ( ph /\ (/) e. dom G ) -> ( T ` (/) ) : ( H ` (/) ) -1-1-onto-> (/) )
95 1 64 65 4 5 6 7 8 9 66 83 94 cnfcomlem 
 |-  ( ( ph /\ (/) e. dom G ) -> ( T ` suc (/) ) : ( H ` suc (/) ) -1-1-onto-> ( ( _om ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) )
96 95 ex 
 |-  ( ph -> ( (/) e. dom G -> ( T ` suc (/) ) : ( H ` suc (/) ) -1-1-onto-> ( ( _om ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) ) )
97 5 oicl 
 |-  Ord dom G
98 ordtr 
 |-  ( Ord dom G -> Tr dom G )
99 97 98 ax-mp 
 |-  Tr dom G
100 trsuc 
 |-  ( ( Tr dom G /\ suc y e. dom G ) -> y e. dom G )
101 99 100 mpan 
 |-  ( suc y e. dom G -> y e. dom G )
102 101 imim1i 
 |-  ( ( y e. dom G -> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) -> ( suc y e. dom G -> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) )
103 2 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> A e. On )
104 3 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> B e. ( _om ^o A ) )
105 simprl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> suc y e. dom G )
106 74 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> A C_ On )
107 72 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( F supp (/) ) C_ A )
108 76 ffvelrni 
 |-  ( suc y e. dom G -> ( G ` suc y ) e. ( F supp (/) ) )
109 108 ad2antrl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( G ` suc y ) e. ( F supp (/) ) )
110 107 109 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( G ` suc y ) e. A )
111 106 110 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( G ` suc y ) e. On )
112 eloni 
 |-  ( ( G ` suc y ) e. On -> Ord ( G ` suc y ) )
113 111 112 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> Ord ( G ` suc y ) )
114 vex 
 |-  y e. _V
115 114 sucid 
 |-  y e. suc y
116 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
117 19 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
118 5 oiiso 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
119 116 117 118 syl2anc 
 |-  ( ph -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
120 119 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
121 101 ad2antrl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> y e. dom G )
122 isorel 
 |-  ( ( G Isom _E , _E ( dom G , ( F supp (/) ) ) /\ ( y e. dom G /\ suc y e. dom G ) ) -> ( y _E suc y <-> ( G ` y ) _E ( G ` suc y ) ) )
123 120 121 105 122 syl12anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( y _E suc y <-> ( G ` y ) _E ( G ` suc y ) ) )
124 114 sucex 
 |-  suc y e. _V
125 124 epeli 
 |-  ( y _E suc y <-> y e. suc y )
126 fvex 
 |-  ( G ` suc y ) e. _V
127 126 epeli 
 |-  ( ( G ` y ) _E ( G ` suc y ) <-> ( G ` y ) e. ( G ` suc y ) )
128 123 125 127 3bitr3g 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( y e. suc y <-> ( G ` y ) e. ( G ` suc y ) ) )
129 115 128 mpbii 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( G ` y ) e. ( G ` suc y ) )
130 ordsucss 
 |-  ( Ord ( G ` suc y ) -> ( ( G ` y ) e. ( G ` suc y ) -> suc ( G ` y ) C_ ( G ` suc y ) ) )
131 113 129 130 sylc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> suc ( G ` y ) C_ ( G ` suc y ) )
132 76 ffvelrni 
 |-  ( y e. dom G -> ( G ` y ) e. ( F supp (/) ) )
133 121 132 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( G ` y ) e. ( F supp (/) ) )
134 107 133 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( G ` y ) e. A )
135 106 134 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( G ` y ) e. On )
136 suceloni 
 |-  ( ( G ` y ) e. On -> suc ( G ` y ) e. On )
137 135 136 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> suc ( G ` y ) e. On )
138 11 a1i 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> _om e. On )
139 80 a1i 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> (/) e. _om )
140 oewordi 
 |-  ( ( ( suc ( G ` y ) e. On /\ ( G ` suc y ) e. On /\ _om e. On ) /\ (/) e. _om ) -> ( suc ( G ` y ) C_ ( G ` suc y ) -> ( _om ^o suc ( G ` y ) ) C_ ( _om ^o ( G ` suc y ) ) ) )
141 137 111 138 139 140 syl31anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( suc ( G ` y ) C_ ( G ` suc y ) -> ( _om ^o suc ( G ` y ) ) C_ ( _om ^o ( G ` suc y ) ) ) )
142 131 141 mpd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( _om ^o suc ( G ` y ) ) C_ ( _om ^o ( G ` suc y ) ) )
143 71 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> F : A --> _om )
144 143 134 ffvelrnd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( F ` ( G ` y ) ) e. _om )
145 nnon 
 |-  ( ( F ` ( G ` y ) ) e. _om -> ( F ` ( G ` y ) ) e. On )
146 144 145 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( F ` ( G ` y ) ) e. On )
147 oecl 
 |-  ( ( _om e. On /\ ( G ` y ) e. On ) -> ( _om ^o ( G ` y ) ) e. On )
148 138 135 147 syl2anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( _om ^o ( G ` y ) ) e. On )
149 oen0 
 |-  ( ( ( _om e. On /\ ( G ` y ) e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o ( G ` y ) ) )
150 138 135 139 149 syl21anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> (/) e. ( _om ^o ( G ` y ) ) )
151 omord2 
 |-  ( ( ( ( F ` ( G ` y ) ) e. On /\ _om e. On /\ ( _om ^o ( G ` y ) ) e. On ) /\ (/) e. ( _om ^o ( G ` y ) ) ) -> ( ( F ` ( G ` y ) ) e. _om <-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. ( ( _om ^o ( G ` y ) ) .o _om ) ) )
152 146 138 148 150 151 syl31anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( ( F ` ( G ` y ) ) e. _om <-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. ( ( _om ^o ( G ` y ) ) .o _om ) ) )
153 144 152 mpbid 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. ( ( _om ^o ( G ` y ) ) .o _om ) )
154 oesuc 
 |-  ( ( _om e. On /\ ( G ` y ) e. On ) -> ( _om ^o suc ( G ` y ) ) = ( ( _om ^o ( G ` y ) ) .o _om ) )
155 138 135 154 syl2anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( _om ^o suc ( G ` y ) ) = ( ( _om ^o ( G ` y ) ) .o _om ) )
156 153 155 eleqtrrd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. ( _om ^o suc ( G ` y ) ) )
157 142 156 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. ( _om ^o ( G ` suc y ) ) )
158 simprr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) )
159 1 103 104 4 5 6 7 8 9 105 157 158 cnfcomlem 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) ) -> ( T ` suc suc y ) : ( H ` suc suc y ) -1-1-onto-> ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) )
160 159 exp32 
 |-  ( ( ph /\ y e. _om ) -> ( suc y e. dom G -> ( ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) -> ( T ` suc suc y ) : ( H ` suc suc y ) -1-1-onto-> ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) ) ) )
161 160 a2d 
 |-  ( ( ph /\ y e. _om ) -> ( ( suc y e. dom G -> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) -> ( suc y e. dom G -> ( T ` suc suc y ) : ( H ` suc suc y ) -1-1-onto-> ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) ) ) )
162 102 161 syl5 
 |-  ( ( ph /\ y e. _om ) -> ( ( y e. dom G -> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) -> ( suc y e. dom G -> ( T ` suc suc y ) : ( H ` suc suc y ) -1-1-onto-> ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) ) ) )
163 162 expcom 
 |-  ( y e. _om -> ( ph -> ( ( y e. dom G -> ( T ` suc y ) : ( H ` suc y ) -1-1-onto-> ( ( _om ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) ) -> ( suc y e. dom G -> ( T ` suc suc y ) : ( H ` suc suc y ) -1-1-onto-> ( ( _om ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) ) ) ) )
164 43 53 63 96 163 finds2 
 |-  ( w e. _om -> ( ph -> ( w e. dom G -> ( T ` suc w ) : ( H ` suc w ) -1-1-onto-> ( ( _om ^o ( G ` w ) ) .o ( F ` ( G ` w ) ) ) ) ) )
165 33 164 vtoclga 
 |-  ( I e. _om -> ( ph -> ( I e. dom G -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) ) )
166 22 165 mpcom 
 |-  ( ph -> ( I e. dom G -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) ) )
167 10 166 mpd 
 |-  ( ph -> ( T ` suc I ) : ( H ` suc I ) -1-1-onto-> ( ( _om ^o ( G ` I ) ) .o ( F ` ( G ` I ) ) ) )