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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
cantnfcl.g ⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
cantnfcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
cantnfval.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
cantnflt.a ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
cantnflt.k ⊢ ( 𝜑 → 𝐾 ∈ suc dom 𝐺 )
cantnflt.c ⊢ ( 𝜑 → 𝐶 ∈ On )
cantnflt.s ⊢ ( 𝜑 → ( 𝐺 “ 𝐾 ) ⊆ 𝐶 )
Assertion cantnflt ( 𝜑 → ( 𝐻 ‘ 𝐾 ) ∈ ( 𝐴 ↑o 𝐶 ) )

Proof

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