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 ) ) ) ) |