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	ffvelcdmi	⊢ ( 𝑥 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 supp ∅ ) )
60	58 59	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝐾 = suc 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐹 supp ∅ ) )
61	53 60	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝐾 = suc 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ On )
62		onsuc	⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ 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	ffvelcdmi	⊢ ( ∅ ∈ dom 𝐺 → ( 𝐺 ‘ ∅ ) ∈ ( 𝐹 supp ∅ ) )
101	49	sselda	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ ∅ ) ∈ ( 𝐹 supp ∅ ) ) → ( 𝐺 ‘ ∅ ) ∈ 𝐵 )
102	100 101	sylan2	⊢ ( ( 𝜑 ∧ ∅ ∈ dom 𝐺 ) → ( 𝐺 ‘ ∅ ) ∈ 𝐵 )
103	99 102	ffvelcdmd	⊢ ( ( 𝜑 ∧ ∅ ∈ 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	ffvelcdmi	⊢ ( 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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( 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		onsuc	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 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	ffvelcdmi	⊢ ( 𝑦 ∈ dom 𝐺 → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
186	175 185	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝐻 ‘ suc 𝑦 ) ∈ ( 𝐴 ↑o suc ( 𝐺 ‘ 𝑦 ) ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝐹 supp ∅ ) )
187	152 186	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ω ) ∧ ( suc 𝑦 ∈ dom 𝐺 ∧ ( 𝐻 ‘ suc 𝑦 ) ∈ ( 𝐴 ↑o suc ( 𝐺 ‘ 𝑦 ) ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ On )
188		onsuc	⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ 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	ffvelcdmi	⊢ ( 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 𝐶 ) )