Metamath Proof Explorer

Theorem cantnflt

Description: An upper bound on the partial sums of the CNF function. Since each term dominates all previous terms, by induction we can bound the whole sum with any exponent A ^o C where C is larger than any exponent ( Gx ) , x e. K which has been summed so far. (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 29-Jun-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfcl.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cantnfcl.f 
|- ( ph -> F e. S )
cantnfval.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
cantnflt.a 
|- ( ph -> (/) e. A )
cantnflt.k 
|- ( ph -> K e. suc dom G )
cantnflt.c 
|- ( ph -> C e. On )
cantnflt.s 
|- ( ph -> ( G " K ) C_ C )
Assertion cantnflt 
|- ( ph -> ( H ` K ) e. ( A ^o C ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 cantnfcl.g 
 |-  G = OrdIso ( _E , ( F supp (/) ) )
5 cantnfcl.f 
 |-  ( ph -> F e. S )
6 cantnfval.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
7 cantnflt.a 
 |-  ( ph -> (/) e. A )
8 cantnflt.k 
 |-  ( ph -> K e. suc dom G )
9 cantnflt.c 
 |-  ( ph -> C e. On )
10 cantnflt.s 
 |-  ( ph -> ( G " K ) C_ C )
11 oen0 
 |-  ( ( ( A e. On /\ C e. On ) /\ (/) e. A ) -> (/) e. ( A ^o C ) )
12 2 9 7 11 syl21anc 
 |-  ( ph -> (/) e. ( A ^o C ) )
13 fveq2 
 |-  ( K = (/) -> ( H ` K ) = ( H ` (/) ) )
14 0ex 
 |-  (/) e. _V
15 6 seqom0g 
 |-  ( (/) e. _V -> ( H ` (/) ) = (/) )
16 14 15 ax-mp 
 |-  ( H ` (/) ) = (/)
17 13 16 eqtrdi 
 |-  ( K = (/) -> ( H ` K ) = (/) )
18 17 eleq1d 
 |-  ( K = (/) -> ( ( H ` K ) e. ( A ^o C ) <-> (/) e. ( A ^o C ) ) )
19 12 18 syl5ibrcom 
 |-  ( ph -> ( K = (/) -> ( H ` K ) e. ( A ^o C ) ) )
20 9 adantr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> C e. On )
21 eloni 
 |-  ( C e. On -> Ord C )
22 20 21 syl 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> Ord C )
23 10 adantr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( G " K ) C_ C )
24 4 oif 
 |-  G : dom G --> ( F supp (/) )
25 ffn 
 |-  ( G : dom G --> ( F supp (/) ) -> G Fn dom G )
26 24 25 mp1i 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> G Fn dom G )
27 4 oicl 
 |-  Ord dom G
28 ordsuc 
 |-  ( Ord dom G <-> Ord suc dom G )
29 27 28 mpbi 
 |-  Ord suc dom G
30 ordelon 
 |-  ( ( Ord suc dom G /\ K e. suc dom G ) -> K e. On )
31 29 8 30 sylancr 
 |-  ( ph -> K e. On )
32 ordsssuc 
 |-  ( ( K e. On /\ Ord dom G ) -> ( K C_ dom G <-> K e. suc dom G ) )
33 31 27 32 sylancl 
 |-  ( ph -> ( K C_ dom G <-> K e. suc dom G ) )
34 8 33 mpbird 
 |-  ( ph -> K C_ dom G )
35 34 adantr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> K C_ dom G )
36 vex 
 |-  x e. _V
37 36 sucid 
 |-  x e. suc x
38 simprr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> K = suc x )
39 37 38 eleqtrrid 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> x e. K )
40 fnfvima 
 |-  ( ( G Fn dom G /\ K C_ dom G /\ x e. K ) -> ( G ` x ) e. ( G " K ) )
41 26 35 39 40 syl3anc 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( G ` x ) e. ( G " K ) )
42 23 41 sseldd 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( G ` x ) e. C )
43 ordsucss 
 |-  ( Ord C -> ( ( G ` x ) e. C -> suc ( G ` x ) C_ C ) )
44 22 42 43 sylc 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> suc ( G ` x ) C_ C )
45 suppssdm 
 |-  ( F supp (/) ) C_ dom F
46 1 2 3 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )
47 5 46 mpbid 
 |-  ( ph -> ( F : B --> A /\ F finSupp (/) ) )
48 47 simpld 
 |-  ( ph -> F : B --> A )
49 45 48 fssdm 
 |-  ( ph -> ( F supp (/) ) C_ B )
50 onss 
 |-  ( B e. On -> B C_ On )
51 3 50 syl 
 |-  ( ph -> B C_ On )
52 49 51 sstrd 
 |-  ( ph -> ( F supp (/) ) C_ On )
53 52 adantr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( F supp (/) ) C_ On )
54 8 adantr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> K e. suc dom G )
55 38 54 eqeltrrd 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> suc x e. suc dom G )
56 ordsucelsuc 
 |-  ( Ord dom G -> ( x e. dom G <-> suc x e. suc dom G ) )
57 27 56 ax-mp 
 |-  ( x e. dom G <-> suc x e. suc dom G )
58 55 57 sylibr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> x e. dom G )
59 24 ffvelrni 
 |-  ( x e. dom G -> ( G ` x ) e. ( F supp (/) ) )
60 58 59 syl 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( G ` x ) e. ( F supp (/) ) )
61 53 60 sseldd 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( G ` x ) e. On )
62 suceloni 
 |-  ( ( G ` x ) e. On -> suc ( G ` x ) e. On )
63 61 62 syl 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> suc ( G ` x ) e. On )
64 2 adantr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> A e. On )
65 7 adantr 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> (/) e. A )
66 oewordi 
 |-  ( ( ( suc ( G ` x ) e. On /\ C e. On /\ A e. On ) /\ (/) e. A ) -> ( suc ( G ` x ) C_ C -> ( A ^o suc ( G ` x ) ) C_ ( A ^o C ) ) )
67 63 20 64 65 66 syl31anc 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( suc ( G ` x ) C_ C -> ( A ^o suc ( G ` x ) ) C_ ( A ^o C ) ) )
68 44 67 mpd 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( A ^o suc ( G ` x ) ) C_ ( A ^o C ) )
69 38 fveq2d 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( H ` K ) = ( H ` suc x ) )
70 simprl 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> x e. _om )
71 simpl 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ph )
72 eleq1 
 |-  ( x = (/) -> ( x e. dom G <-> (/) e. dom G ) )
73 suceq 
 |-  ( x = (/) -> suc x = suc (/) )
74 73 fveq2d 
 |-  ( x = (/) -> ( H ` suc x ) = ( H ` suc (/) ) )
75 fveq2 
 |-  ( x = (/) -> ( G ` x ) = ( G ` (/) ) )
76 suceq 
 |-  ( ( G ` x ) = ( G ` (/) ) -> suc ( G ` x ) = suc ( G ` (/) ) )
77 75 76 syl 
 |-  ( x = (/) -> suc ( G ` x ) = suc ( G ` (/) ) )
78 77 oveq2d 
 |-  ( x = (/) -> ( A ^o suc ( G ` x ) ) = ( A ^o suc ( G ` (/) ) ) )
79 74 78 eleq12d 
 |-  ( x = (/) -> ( ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) <-> ( H ` suc (/) ) e. ( A ^o suc ( G ` (/) ) ) ) )
80 72 79 imbi12d 
 |-  ( x = (/) -> ( ( x e. dom G -> ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) ) <-> ( (/) e. dom G -> ( H ` suc (/) ) e. ( A ^o suc ( G ` (/) ) ) ) ) )
81 eleq1 
 |-  ( x = y -> ( x e. dom G <-> y e. dom G ) )
82 suceq 
 |-  ( x = y -> suc x = suc y )
83 82 fveq2d 
 |-  ( x = y -> ( H ` suc x ) = ( H ` suc y ) )
84 fveq2 
 |-  ( x = y -> ( G ` x ) = ( G ` y ) )
85 suceq 
 |-  ( ( G ` x ) = ( G ` y ) -> suc ( G ` x ) = suc ( G ` y ) )
86 84 85 syl 
 |-  ( x = y -> suc ( G ` x ) = suc ( G ` y ) )
87 86 oveq2d 
 |-  ( x = y -> ( A ^o suc ( G ` x ) ) = ( A ^o suc ( G ` y ) ) )
88 83 87 eleq12d 
 |-  ( x = y -> ( ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) <-> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) )
89 81 88 imbi12d 
 |-  ( x = y -> ( ( x e. dom G -> ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) ) <-> ( y e. dom G -> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) )
90 eleq1 
 |-  ( x = suc y -> ( x e. dom G <-> suc y e. dom G ) )
91 suceq 
 |-  ( x = suc y -> suc x = suc suc y )
92 91 fveq2d 
 |-  ( x = suc y -> ( H ` suc x ) = ( H ` suc suc y ) )
93 fveq2 
 |-  ( x = suc y -> ( G ` x ) = ( G ` suc y ) )
94 suceq 
 |-  ( ( G ` x ) = ( G ` suc y ) -> suc ( G ` x ) = suc ( G ` suc y ) )
95 93 94 syl 
 |-  ( x = suc y -> suc ( G ` x ) = suc ( G ` suc y ) )
96 95 oveq2d 
 |-  ( x = suc y -> ( A ^o suc ( G ` x ) ) = ( A ^o suc ( G ` suc y ) ) )
97 92 96 eleq12d 
 |-  ( x = suc y -> ( ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) <-> ( H ` suc suc y ) e. ( A ^o suc ( G ` suc y ) ) ) )
98 90 97 imbi12d 
 |-  ( x = suc y -> ( ( x e. dom G -> ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) ) <-> ( suc y e. dom G -> ( H ` suc suc y ) e. ( A ^o suc ( G ` suc y ) ) ) ) )
99 48 adantr 
 |-  ( ( ph /\ (/) e. dom G ) -> F : B --> A )
100 24 ffvelrni 
 |-  ( (/) e. dom G -> ( G ` (/) ) e. ( F supp (/) ) )
101 49 sselda 
 |-  ( ( ph /\ ( G ` (/) ) e. ( F supp (/) ) ) -> ( G ` (/) ) e. B )
102 100 101 sylan2 
 |-  ( ( ph /\ (/) e. dom G ) -> ( G ` (/) ) e. B )
103 99 102 ffvelrnd 
 |-  ( ( ph /\ (/) e. dom G ) -> ( F ` ( G ` (/) ) ) e. A )
104 2 adantr 
 |-  ( ( ph /\ (/) e. dom G ) -> A e. On )
105 onelon 
 |-  ( ( A e. On /\ ( F ` ( G ` (/) ) ) e. A ) -> ( F ` ( G ` (/) ) ) e. On )
106 104 103 105 syl2anc 
 |-  ( ( ph /\ (/) e. dom G ) -> ( F ` ( G ` (/) ) ) e. On )
107 52 sselda 
 |-  ( ( ph /\ ( G ` (/) ) e. ( F supp (/) ) ) -> ( G ` (/) ) e. On )
108 100 107 sylan2 
 |-  ( ( ph /\ (/) e. dom G ) -> ( G ` (/) ) e. On )
109 oecl 
 |-  ( ( A e. On /\ ( G ` (/) ) e. On ) -> ( A ^o ( G ` (/) ) ) e. On )
110 104 108 109 syl2anc 
 |-  ( ( ph /\ (/) e. dom G ) -> ( A ^o ( G ` (/) ) ) e. On )
111 7 adantr 
 |-  ( ( ph /\ (/) e. dom G ) -> (/) e. A )
112 oen0 
 |-  ( ( ( A e. On /\ ( G ` (/) ) e. On ) /\ (/) e. A ) -> (/) e. ( A ^o ( G ` (/) ) ) )
113 104 108 111 112 syl21anc 
 |-  ( ( ph /\ (/) e. dom G ) -> (/) e. ( A ^o ( G ` (/) ) ) )
114 omord2 
 |-  ( ( ( ( F ` ( G ` (/) ) ) e. On /\ A e. On /\ ( A ^o ( G ` (/) ) ) e. On ) /\ (/) e. ( A ^o ( G ` (/) ) ) ) -> ( ( F ` ( G ` (/) ) ) e. A <-> ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) e. ( ( A ^o ( G ` (/) ) ) .o A ) ) )
115 106 104 110 113 114 syl31anc 
 |-  ( ( ph /\ (/) e. dom G ) -> ( ( F ` ( G ` (/) ) ) e. A <-> ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) e. ( ( A ^o ( G ` (/) ) ) .o A ) ) )
116 103 115 mpbid 
 |-  ( ( ph /\ (/) e. dom G ) -> ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) e. ( ( A ^o ( G ` (/) ) ) .o A ) )
117 peano1 
 |-  (/) e. _om
118 117 a1i 
 |-  ( (/) e. dom G -> (/) e. _om )
119 1 2 3 4 5 6 cantnfsuc 
 |-  ( ( ph /\ (/) e. _om ) -> ( H ` suc (/) ) = ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) +o ( H ` (/) ) ) )
120 118 119 sylan2 
 |-  ( ( ph /\ (/) e. dom G ) -> ( H ` suc (/) ) = ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) +o ( H ` (/) ) ) )
121 16 oveq2i 
 |-  ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) +o ( H ` (/) ) ) = ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) +o (/) )
122 omcl 
 |-  ( ( ( A ^o ( G ` (/) ) ) e. On /\ ( F ` ( G ` (/) ) ) e. On ) -> ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) e. On )
123 110 106 122 syl2anc 
 |-  ( ( ph /\ (/) e. dom G ) -> ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) e. On )
124 oa0 
 |-  ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) e. On -> ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) +o (/) ) = ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) )
125 123 124 syl 
 |-  ( ( ph /\ (/) e. dom G ) -> ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) +o (/) ) = ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) )
126 121 125 eqtrid 
 |-  ( ( ph /\ (/) e. dom G ) -> ( ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) +o ( H ` (/) ) ) = ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) )
127 120 126 eqtrd 
 |-  ( ( ph /\ (/) e. dom G ) -> ( H ` suc (/) ) = ( ( A ^o ( G ` (/) ) ) .o ( F ` ( G ` (/) ) ) ) )
128 oesuc 
 |-  ( ( A e. On /\ ( G ` (/) ) e. On ) -> ( A ^o suc ( G ` (/) ) ) = ( ( A ^o ( G ` (/) ) ) .o A ) )
129 104 108 128 syl2anc 
 |-  ( ( ph /\ (/) e. dom G ) -> ( A ^o suc ( G ` (/) ) ) = ( ( A ^o ( G ` (/) ) ) .o A ) )
130 116 127 129 3eltr4d 
 |-  ( ( ph /\ (/) e. dom G ) -> ( H ` suc (/) ) e. ( A ^o suc ( G ` (/) ) ) )
131 130 ex 
 |-  ( ph -> ( (/) e. dom G -> ( H ` suc (/) ) e. ( A ^o suc ( G ` (/) ) ) ) )
132 ordtr 
 |-  ( Ord dom G -> Tr dom G )
133 27 132 ax-mp 
 |-  Tr dom G
134 trsuc 
 |-  ( ( Tr dom G /\ suc y e. dom G ) -> y e. dom G )
135 133 134 mpan 
 |-  ( suc y e. dom G -> y e. dom G )
136 135 imim1i 
 |-  ( ( y e. dom G -> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) -> ( suc y e. dom G -> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) )
137 2 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> A e. On )
138 eloni 
 |-  ( A e. On -> Ord A )
139 137 138 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> Ord A )
140 48 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> F : B --> A )
141 49 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( F supp (/) ) C_ B )
142 24 ffvelrni 
 |-  ( suc y e. dom G -> ( G ` suc y ) e. ( F supp (/) ) )
143 142 ad2antrl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( G ` suc y ) e. ( F supp (/) ) )
144 141 143 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( G ` suc y ) e. B )
145 140 144 ffvelrnd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( F ` ( G ` suc y ) ) e. A )
146 ordsucss 
 |-  ( Ord A -> ( ( F ` ( G ` suc y ) ) e. A -> suc ( F ` ( G ` suc y ) ) C_ A ) )
147 139 145 146 sylc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> suc ( F ` ( G ` suc y ) ) C_ A )
148 onelon 
 |-  ( ( A e. On /\ ( F ` ( G ` suc y ) ) e. A ) -> ( F ` ( G ` suc y ) ) e. On )
149 137 145 148 syl2anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( F ` ( G ` suc y ) ) e. On )
150 suceloni 
 |-  ( ( F ` ( G ` suc y ) ) e. On -> suc ( F ` ( G ` suc y ) ) e. On )
151 149 150 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> suc ( F ` ( G ` suc y ) ) e. On )
152 52 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( F supp (/) ) C_ On )
153 152 143 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( G ` suc y ) e. On )
154 oecl 
 |-  ( ( A e. On /\ ( G ` suc y ) e. On ) -> ( A ^o ( G ` suc y ) ) e. On )
155 137 153 154 syl2anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( A ^o ( G ` suc y ) ) e. On )
156 omwordi 
 |-  ( ( suc ( F ` ( G ` suc y ) ) e. On /\ A e. On /\ ( A ^o ( G ` suc y ) ) e. On ) -> ( suc ( F ` ( G ` suc y ) ) C_ A -> ( ( A ^o ( G ` suc y ) ) .o suc ( F ` ( G ` suc y ) ) ) C_ ( ( A ^o ( G ` suc y ) ) .o A ) ) )
157 151 137 155 156 syl3anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( suc ( F ` ( G ` suc y ) ) C_ A -> ( ( A ^o ( G ` suc y ) ) .o suc ( F ` ( G ` suc y ) ) ) C_ ( ( A ^o ( G ` suc y ) ) .o A ) ) )
158 147 157 mpd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( ( A ^o ( G ` suc y ) ) .o suc ( F ` ( G ` suc y ) ) ) C_ ( ( A ^o ( G ` suc y ) ) .o A ) )
159 oesuc 
 |-  ( ( A e. On /\ ( G ` suc y ) e. On ) -> ( A ^o suc ( G ` suc y ) ) = ( ( A ^o ( G ` suc y ) ) .o A ) )
160 137 153 159 syl2anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( A ^o suc ( G ` suc y ) ) = ( ( A ^o ( G ` suc y ) ) .o A ) )
161 158 160 sseqtrrd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( ( A ^o ( G ` suc y ) ) .o suc ( F ` ( G ` suc y ) ) ) C_ ( A ^o suc ( G ` suc y ) ) )
162 eloni 
 |-  ( ( G ` suc y ) e. On -> Ord ( G ` suc y ) )
163 153 162 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> Ord ( G ` suc y ) )
164 vex 
 |-  y e. _V
165 164 sucid 
 |-  y e. suc y
166 164 sucex 
 |-  suc y e. _V
167 166 epeli 
 |-  ( y _E suc y <-> y e. suc y )
168 165 167 mpbir 
 |-  y _E suc y
169 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
170 1 2 3 4 5 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )
171 170 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
172 4 oiiso 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
173 169 171 172 syl2anc 
 |-  ( ph -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
174 173 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
175 135 ad2antrl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> y e. dom G )
176 simprl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> suc y e. dom G )
177 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 ) ) )
178 174 175 176 177 syl12anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( y _E suc y <-> ( G ` y ) _E ( G ` suc y ) ) )
179 168 178 mpbii 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( G ` y ) _E ( G ` suc y ) )
180 fvex 
 |-  ( G ` suc y ) e. _V
181 180 epeli 
 |-  ( ( G ` y ) _E ( G ` suc y ) <-> ( G ` y ) e. ( G ` suc y ) )
182 179 181 sylib 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( G ` y ) e. ( G ` suc y ) )
183 ordsucss 
 |-  ( Ord ( G ` suc y ) -> ( ( G ` y ) e. ( G ` suc y ) -> suc ( G ` y ) C_ ( G ` suc y ) ) )
184 163 182 183 sylc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> suc ( G ` y ) C_ ( G ` suc y ) )
185 24 ffvelrni 
 |-  ( y e. dom G -> ( G ` y ) e. ( F supp (/) ) )
186 175 185 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( G ` y ) e. ( F supp (/) ) )
187 152 186 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( G ` y ) e. On )
188 suceloni 
 |-  ( ( G ` y ) e. On -> suc ( G ` y ) e. On )
189 187 188 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> suc ( G ` y ) e. On )
190 7 ad2antrr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> (/) e. A )
191 oewordi 
 |-  ( ( ( suc ( G ` y ) e. On /\ ( G ` suc y ) e. On /\ A e. On ) /\ (/) e. A ) -> ( suc ( G ` y ) C_ ( G ` suc y ) -> ( A ^o suc ( G ` y ) ) C_ ( A ^o ( G ` suc y ) ) ) )
192 189 153 137 190 191 syl31anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( suc ( G ` y ) C_ ( G ` suc y ) -> ( A ^o suc ( G ` y ) ) C_ ( A ^o ( G ` suc y ) ) ) )
193 184 192 mpd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( A ^o suc ( G ` y ) ) C_ ( A ^o ( G ` suc y ) ) )
194 simprr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) )
195 193 194 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( H ` suc y ) e. ( A ^o ( G ` suc y ) ) )
196 peano2 
 |-  ( y e. _om -> suc y e. _om )
197 196 ad2antlr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> suc y e. _om )
198 6 cantnfvalf 
 |-  H : _om --> On
199 198 ffvelrni 
 |-  ( suc y e. _om -> ( H ` suc y ) e. On )
200 197 199 syl 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( H ` suc y ) e. On )
201 omcl 
 |-  ( ( ( A ^o ( G ` suc y ) ) e. On /\ ( F ` ( G ` suc y ) ) e. On ) -> ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) e. On )
202 155 149 201 syl2anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) e. On )
203 oaord 
 |-  ( ( ( H ` suc y ) e. On /\ ( A ^o ( G ` suc y ) ) e. On /\ ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) e. On ) -> ( ( H ` suc y ) e. ( A ^o ( G ` suc y ) ) <-> ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( H ` suc y ) ) e. ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( A ^o ( G ` suc y ) ) ) ) )
204 200 155 202 203 syl3anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( ( H ` suc y ) e. ( A ^o ( G ` suc y ) ) <-> ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( H ` suc y ) ) e. ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( A ^o ( G ` suc y ) ) ) ) )
205 195 204 mpbid 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( H ` suc y ) ) e. ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( A ^o ( G ` suc y ) ) ) )
206 1 2 3 4 5 6 cantnfsuc 
 |-  ( ( ph /\ suc y e. _om ) -> ( H ` suc suc y ) = ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( H ` suc y ) ) )
207 196 206 sylan2 
 |-  ( ( ph /\ y e. _om ) -> ( H ` suc suc y ) = ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( H ` suc y ) ) )
208 207 adantr 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( H ` suc suc y ) = ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( H ` suc y ) ) )
209 omsuc 
 |-  ( ( ( A ^o ( G ` suc y ) ) e. On /\ ( F ` ( G ` suc y ) ) e. On ) -> ( ( A ^o ( G ` suc y ) ) .o suc ( F ` ( G ` suc y ) ) ) = ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( A ^o ( G ` suc y ) ) ) )
210 155 149 209 syl2anc 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( ( A ^o ( G ` suc y ) ) .o suc ( F ` ( G ` suc y ) ) ) = ( ( ( A ^o ( G ` suc y ) ) .o ( F ` ( G ` suc y ) ) ) +o ( A ^o ( G ` suc y ) ) ) )
211 205 208 210 3eltr4d 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( H ` suc suc y ) e. ( ( A ^o ( G ` suc y ) ) .o suc ( F ` ( G ` suc y ) ) ) )
212 161 211 sseldd 
 |-  ( ( ( ph /\ y e. _om ) /\ ( suc y e. dom G /\ ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) ) -> ( H ` suc suc y ) e. ( A ^o suc ( G ` suc y ) ) )
213 212 exp32 
 |-  ( ( ph /\ y e. _om ) -> ( suc y e. dom G -> ( ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) -> ( H ` suc suc y ) e. ( A ^o suc ( G ` suc y ) ) ) ) )
214 213 a2d 
 |-  ( ( ph /\ y e. _om ) -> ( ( suc y e. dom G -> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) -> ( suc y e. dom G -> ( H ` suc suc y ) e. ( A ^o suc ( G ` suc y ) ) ) ) )
215 136 214 syl5 
 |-  ( ( ph /\ y e. _om ) -> ( ( y e. dom G -> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) -> ( suc y e. dom G -> ( H ` suc suc y ) e. ( A ^o suc ( G ` suc y ) ) ) ) )
216 215 expcom 
 |-  ( y e. _om -> ( ph -> ( ( y e. dom G -> ( H ` suc y ) e. ( A ^o suc ( G ` y ) ) ) -> ( suc y e. dom G -> ( H ` suc suc y ) e. ( A ^o suc ( G ` suc y ) ) ) ) ) )
217 80 89 98 131 216 finds2 
 |-  ( x e. _om -> ( ph -> ( x e. dom G -> ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) ) ) )
218 70 71 58 217 syl3c 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( H ` suc x ) e. ( A ^o suc ( G ` x ) ) )
219 69 218 eqeltrd 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( H ` K ) e. ( A ^o suc ( G ` x ) ) )
220 68 219 sseldd 
 |-  ( ( ph /\ ( x e. _om /\ K = suc x ) ) -> ( H ` K ) e. ( A ^o C ) )
221 220 rexlimdvaa 
 |-  ( ph -> ( E. x e. _om K = suc x -> ( H ` K ) e. ( A ^o C ) ) )
222 peano2 
 |-  ( dom G e. _om -> suc dom G e. _om )
223 170 222 simpl2im 
 |-  ( ph -> suc dom G e. _om )
224 elnn 
 |-  ( ( K e. suc dom G /\ suc dom G e. _om ) -> K e. _om )
225 8 223 224 syl2anc 
 |-  ( ph -> K e. _om )
226 nn0suc 
 |-  ( K e. _om -> ( K = (/) \/ E. x e. _om K = suc x ) )
227 225 226 syl 
 |-  ( ph -> ( K = (/) \/ E. x e. _om K = suc x ) )
228 19 221 227 mpjaod 
 |-  ( ph -> ( H ` K ) e. ( A ^o C ) )