cantnflt - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cantnflt		Structured version Visualization version GIF version

Theorem cantnflt 9360

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 𝐴 ↑_o 𝐶 where 𝐶 is larger than any exponent (𝐺‘𝑥), 𝑥 ∈ 𝐾 which has been summed so far. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 29-Jun-2019.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
cantnflt	⊢ (𝜑 → (𝐻‘𝐾) ∈ (𝐴 ↑_o 𝐶))

Distinct variable groups: 𝑧,𝑘,𝐵 𝑧,𝐶 𝐴,𝑘,𝑧 𝑘,𝐹,𝑧 𝑆,𝑘,𝑧 𝑘,𝐺,𝑧 𝑘,𝐾,𝑧 𝜑,𝑘,𝑧 Allowed substitution hints: 𝐶(𝑘) 𝐻(𝑧,𝑘)

Proof of Theorem cantnflt Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cantnfs.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ On)
2		cantnflt.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ On)
3		cantnflt.a	. . . 4 ⊢ (𝜑 → ∅ ∈ 𝐴)
4		oen0 8379	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_o 𝐶))
5	1, 2, 3, 4	syl21anc 834	. . 3 ⊢ (𝜑 → ∅ ∈ (𝐴 ↑_o 𝐶))
6		fveq2 6756	. . . . 5 ⊢ (𝐾 = ∅ → (𝐻‘𝐾) = (𝐻‘∅))
7		0ex 5226	. . . . . 6 ⊢ ∅ ∈ V
8		cantnfval.h	. . . . . . 7 ⊢ 𝐻 = seq_ω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑_o (𝐺‘𝑘)) ·_o (𝐹‘(𝐺‘𝑘))) +_o 𝑧)), ∅)
9	8	seqom0g 8257	. . . . . 6 ⊢ (∅ ∈ V → (𝐻‘∅) = ∅)
10	7, 9	ax-mp 5	. . . . 5 ⊢ (𝐻‘∅) = ∅
11	6, 10	eqtrdi 2795	. . . 4 ⊢ (𝐾 = ∅ → (𝐻‘𝐾) = ∅)
12	11	eleq1d 2823	. . 3 ⊢ (𝐾 = ∅ → ((𝐻‘𝐾) ∈ (𝐴 ↑_o 𝐶) ↔ ∅ ∈ (𝐴 ↑_o 𝐶)))
13	5, 12	syl5ibrcom 246	. 2 ⊢ (𝜑 → (𝐾 = ∅ → (𝐻‘𝐾) ∈ (𝐴 ↑_o 𝐶)))
14	2	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15		eloni 6261	. . . . . . 7 ⊢ (𝐶 ∈ On → Ord 𝐶)
16	14, 15	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → Ord 𝐶)
17		cantnflt.s	. . . . . . . 8 ⊢ (𝜑 → (𝐺 “ 𝐾) ⊆ 𝐶)
18	17	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺 “ 𝐾) ⊆ 𝐶)
19		cantnfcl.g	. . . . . . . . . 10 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
20	19	oif 9219	. . . . . . . . 9 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21		ffn 6584	. . . . . . . . 9 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
22	20, 21	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23		cantnflt.k	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ suc dom 𝐺)
24	19	oicl 9218	. . . . . . . . . . . . 13 ⊢ Ord dom 𝐺
25		ordsuc 7636	. . . . . . . . . . . . 13 ⊢ (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
26	24, 25	mpbi 229	. . . . . . . . . . . 12 ⊢ Ord suc dom 𝐺
27		ordelon 6275	. . . . . . . . . . . 12 ⊢ ((Ord suc dom 𝐺 ∧ 𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
28	26, 23, 27	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ On)
29		ordsssuc 6337	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺 ↔ 𝐾 ∈ suc dom 𝐺))
30	28, 24, 29	sylancl 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾 ⊆ dom 𝐺 ↔ 𝐾 ∈ suc dom 𝐺))
31	23, 30	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ⊆ dom 𝐺)
32	31	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33		vex 3426	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
34	33	sucid 6330	. . . . . . . . 9 ⊢ 𝑥 ∈ suc 𝑥
35		simprr 769	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
36	34, 35	eleqtrrid 2846	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ 𝐾)
37		fnfvima 7091	. . . . . . . 8 ⊢ ((𝐺 Fn dom 𝐺 ∧ 𝐾 ⊆ dom 𝐺 ∧ 𝑥 ∈ 𝐾) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐾))
38	22, 32, 36, 37	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐾))
39	18, 38	sseldd 3918	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ 𝐶)
40		ordsucss 7640	. . . . . 6 ⊢ (Ord 𝐶 → ((𝐺‘𝑥) ∈ 𝐶 → suc (𝐺‘𝑥) ⊆ 𝐶))
41	16, 39, 40	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺‘𝑥) ⊆ 𝐶)
42		suppssdm 7964	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
43		cantnfcl.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
44		cantnfs.s	. . . . . . . . . . . . . 14 ⊢ 𝑆 = dom (𝐴 CNF 𝐵)
45		cantnfs.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ On)
46	44, 1, 45	cantnfs 9354	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
47	43, 46	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
48	47	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐵⟶𝐴)
49	42, 48	fssdm 6604	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
50		onss 7611	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
51	45, 50	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ⊆ On)
52	49, 51	sstrd 3927	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
53	52	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
54	23	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
55	35, 54	eqeltrrd 2840	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
56		ordsucelsuc 7644	. . . . . . . . . . 11 ⊢ (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
57	24, 56	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
58	55, 57	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
59	20	ffvelrni 6942	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐺 → (𝐺‘𝑥) ∈ (𝐹 supp ∅))
60	58, 59	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ (𝐹 supp ∅))
61	53, 60	sseldd 3918	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ On)
62		suceloni 7635	. . . . . . 7 ⊢ ((𝐺‘𝑥) ∈ On → suc (𝐺‘𝑥) ∈ On)
63	61, 62	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺‘𝑥) ∈ On)
64	1	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
65	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
66		oewordi 8384	. . . . . 6 ⊢ (((suc (𝐺‘𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺‘𝑥) ⊆ 𝐶 → (𝐴 ↑_o suc (𝐺‘𝑥)) ⊆ (𝐴 ↑_o 𝐶)))
67	63, 14, 64, 65, 66	syl31anc 1371	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺‘𝑥) ⊆ 𝐶 → (𝐴 ↑_o suc (𝐺‘𝑥)) ⊆ (𝐴 ↑_o 𝐶)))
68	41, 67	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴 ↑_o suc (𝐺‘𝑥)) ⊆ (𝐴 ↑_o 𝐶))
69	35	fveq2d 6760	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘𝐾) = (𝐻‘suc 𝑥))
70		simprl 767	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
71		simpl 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
72		eleq1 2826	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
73		suceq 6316	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → suc 𝑥 = suc ∅)
74	73	fveq2d 6760	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
75		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝐺‘𝑥) = (𝐺‘∅))
76		suceq 6316	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑥) = (𝐺‘∅) → suc (𝐺‘𝑥) = suc (𝐺‘∅))
77	75, 76	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → suc (𝐺‘𝑥) = suc (𝐺‘∅))
78	77	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐴 ↑_o suc (𝐺‘𝑥)) = (𝐴 ↑_o suc (𝐺‘∅)))
79	74, 78	eleq12d 2833	. . . . . . . 8 ⊢ (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴 ↑_o suc (𝐺‘∅))))
80	72, 79	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴 ↑_o suc (𝐺‘∅)))))
81		eleq1 2826	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺 ↔ 𝑦 ∈ dom 𝐺))
82		suceq 6316	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
83	82	fveq2d 6760	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
84		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦))
85		suceq 6316	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑥) = (𝐺‘𝑦) → suc (𝐺‘𝑥) = suc (𝐺‘𝑦))
86	84, 85	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → suc (𝐺‘𝑥) = suc (𝐺‘𝑦))
87	86	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ↑_o suc (𝐺‘𝑥)) = (𝐴 ↑_o suc (𝐺‘𝑦)))
88	83, 87	eleq12d 2833	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦))))
89	81, 88	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))))
90		eleq1 2826	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
91		suceq 6316	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
92	91	fveq2d 6760	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
93		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝐺‘𝑥) = (𝐺‘suc 𝑦))
94		suceq 6316	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑥) = (𝐺‘suc 𝑦) → suc (𝐺‘𝑥) = suc (𝐺‘suc 𝑦))
95	93, 94	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → suc (𝐺‘𝑥) = suc (𝐺‘suc 𝑦))
96	95	oveq2d 7271	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐴 ↑_o suc (𝐺‘𝑥)) = (𝐴 ↑_o suc (𝐺‘suc 𝑦)))
97	92, 96	eleq12d 2833	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥)) ↔ (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘suc 𝑦))))
98	90, 97	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘suc 𝑦)))))
99	48	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐹:𝐵⟶𝐴)
100	20	ffvelrni 6942	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
101	49	sselda 3917	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
102	100, 101	sylan2 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
103	99, 102	ffvelrnd 6944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
104	1	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
105		onelon 6276	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
106	104, 103, 105	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
107	52	sselda 3917	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
108	100, 107	sylan2 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
109		oecl 8329	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴 ↑_o (𝐺‘∅)) ∈ On)
110	104, 108, 109	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴 ↑_o (𝐺‘∅)) ∈ On)
111	3	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
112		oen0 8379	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_o (𝐺‘∅)))
113	104, 108, 111, 112	syl21anc 834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴 ↑_o (𝐺‘∅)))
114		omord2 8360	. . . . . . . . . . 11 ⊢ ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ↑_o (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴 ↑_o (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) ∈ ((𝐴 ↑_o (𝐺‘∅)) ·_o 𝐴)))
115	106, 104, 110, 113, 114	syl31anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) ∈ ((𝐴 ↑_o (𝐺‘∅)) ·_o 𝐴)))
116	103, 115	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) ∈ ((𝐴 ↑_o (𝐺‘∅)) ·_o 𝐴))
117		peano1 7710	. . . . . . . . . . . 12 ⊢ ∅ ∈ ω
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (∅ ∈ dom 𝐺 → ∅ ∈ ω)
119	44, 1, 45, 19, 43, 8	cantnfsuc 9358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) +_o (𝐻‘∅)))
120	118, 119	sylan2 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) +_o (𝐻‘∅)))
121	10	oveq2i 7266	. . . . . . . . . . 11 ⊢ (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) +_o (𝐻‘∅)) = (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) +_o ∅)
122		omcl 8328	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↑_o (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) ∈ On)
123	110, 106, 122	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) ∈ On)
124		oa0 8308	. . . . . . . . . . . 12 ⊢ (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) +_o ∅) = ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))))
125	123, 124	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) +_o ∅) = ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))))
126	121, 125	eqtrid 2790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))) +_o (𝐻‘∅)) = ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))))
127	120, 126	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴 ↑_o (𝐺‘∅)) ·_o (𝐹‘(𝐺‘∅))))
128		oesuc 8319	. . . . . . . . . 10 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴 ↑_o suc (𝐺‘∅)) = ((𝐴 ↑_o (𝐺‘∅)) ·_o 𝐴))
129	104, 108, 128	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴 ↑_o suc (𝐺‘∅)) = ((𝐴 ↑_o (𝐺‘∅)) ·_o 𝐴))
130	116, 127, 129	3eltr4d 2854	. . . . . . . 8 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴 ↑_o suc (𝐺‘∅)))
131	130	ex 412	. . . . . . 7 ⊢ (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴 ↑_o suc (𝐺‘∅))))
132		ordtr 6265	. . . . . . . . . . . 12 ⊢ (Ord dom 𝐺 → Tr dom 𝐺)
133	24, 132	ax-mp 5	. . . . . . . . . . 11 ⊢ Tr dom 𝐺
134		trsuc 6335	. . . . . . . . . . 11 ⊢ ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
135	133, 134	mpan 686	. . . . . . . . . 10 ⊢ (suc 𝑦 ∈ dom 𝐺 → 𝑦 ∈ dom 𝐺)
136	135	imim1i 63	. . . . . . . . 9 ⊢ ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦))))
137	1	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → 𝐴 ∈ On)
138		eloni 6261	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On → Ord 𝐴)
139	137, 138	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → Ord 𝐴)
140	48	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → 𝐹:𝐵⟶𝐴)
141	49	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
142	20	ffvelrni 6942	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
143	142	ad2antrl 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
144	141, 143	sseldd 3918	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
145	140, 144	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
146		ordsucss 7640	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
147	139, 145, 146	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
148		onelon 6276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
149	137, 145, 148	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
150		suceloni 7635	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151	149, 150	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
152	52	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐹 supp ∅) ⊆ On)
153	152, 143	sseldd 3918	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
154		oecl 8329	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴 ↑_o (𝐺‘suc 𝑦)) ∈ On)
155	137, 153, 154	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐴 ↑_o (𝐺‘suc 𝑦)) ∈ On)
156		omwordi 8364	. . . . . . . . . . . . . . 15 ⊢ ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ↑_o (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o 𝐴)))
157	151, 137, 155, 156	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o 𝐴)))
158	147, 157	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o 𝐴))
159		oesuc 8319	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴 ↑_o suc (𝐺‘suc 𝑦)) = ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o 𝐴))
160	137, 153, 159	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐴 ↑_o suc (𝐺‘suc 𝑦)) = ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o 𝐴))
161	158, 160	sseqtrrd 3958	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴 ↑_o suc (𝐺‘suc 𝑦)))
162		eloni 6261	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
163	153, 162	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → Ord (𝐺‘suc 𝑦))
164		vex 3426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
165	164	sucid 6330	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ suc 𝑦
166	164	sucex 7633	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc 𝑦 ∈ V
167	166	epeli 5488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 E suc 𝑦 ↔ 𝑦 ∈ suc 𝑦)
168	165, 167	mpbir 230	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑦 E suc 𝑦
169		ovexd 7290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
170	44, 1, 45, 19, 43	cantnfcl 9355	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
171	170	simpld 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → E We (𝐹 supp ∅))
172	19	oiiso 9226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
173	169, 171, 172	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
174	173	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175	135	ad2antrl 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → 𝑦 ∈ dom 𝐺)
176		simprl 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → suc 𝑦 ∈ dom 𝐺)
177		isorel 7177	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺‘𝑦) E (𝐺‘suc 𝑦)))
178	174, 175, 176, 177	syl12anc 833	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺‘𝑦) E (𝐺‘suc 𝑦)))
179	168, 178	mpbii 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐺‘𝑦) E (𝐺‘suc 𝑦))
180		fvex 6769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘suc 𝑦) ∈ V
181	180	epeli 5488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺‘𝑦) ∈ (𝐺‘suc 𝑦))
182	179, 181	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐺‘𝑦) ∈ (𝐺‘suc 𝑦))
183		ordsucss 7640	. . . . . . . . . . . . . . . . 17 ⊢ (Ord (𝐺‘suc 𝑦) → ((𝐺‘𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)))
184	163, 182, 183	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦))
185	20	ffvelrni 6942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ dom 𝐺 → (𝐺‘𝑦) ∈ (𝐹 supp ∅))
186	175, 185	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐺‘𝑦) ∈ (𝐹 supp ∅))
187	152, 186	sseldd 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐺‘𝑦) ∈ On)
188		suceloni 7635	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑦) ∈ On → suc (𝐺‘𝑦) ∈ On)
189	187, 188	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → suc (𝐺‘𝑦) ∈ On)
190	3	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → ∅ ∈ 𝐴)
191		oewordi 8384	. . . . . . . . . . . . . . . . 17 ⊢ (((suc (𝐺‘𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴 ↑_o suc (𝐺‘𝑦)) ⊆ (𝐴 ↑_o (𝐺‘suc 𝑦))))
192	189, 153, 137, 190, 191	syl31anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴 ↑_o suc (𝐺‘𝑦)) ⊆ (𝐴 ↑_o (𝐺‘suc 𝑦))))
193	184, 192	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐴 ↑_o suc (𝐺‘𝑦)) ⊆ (𝐴 ↑_o (𝐺‘suc 𝑦)))
194		simprr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))
195	193, 194	sseldd 3918	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o (𝐺‘suc 𝑦)))
196		peano2 7711	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
197	196	ad2antlr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → suc 𝑦 ∈ ω)
198	8	cantnfvalf 9353	. . . . . . . . . . . . . . . . 17 ⊢ 𝐻:ω⟶On
199	198	ffvelrni 6942	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
200	197, 199	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
201		omcl 8328	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↑_o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
202	155, 149, 201	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
203		oaord 8340	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘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 1369	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (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 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) +_o (𝐻‘suc 𝑦)) ∈ (((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) +_o (𝐴 ↑_o (𝐺‘suc 𝑦))))
206	44, 1, 45, 19, 43, 8	cantnfsuc 9358	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) +_o (𝐻‘suc 𝑦)))
207	196, 206	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) +_o (𝐻‘suc 𝑦)))
208	207	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐻‘suc suc 𝑦) = (((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) +_o (𝐻‘suc 𝑦)))
209		omsuc 8318	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ↑_o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) +_o (𝐴 ↑_o (𝐺‘suc 𝑦))))
210	155, 149, 209	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o (𝐹‘(𝐺‘suc 𝑦))) +_o (𝐴 ↑_o (𝐺‘suc 𝑦))))
211	205, 208, 210	3eltr4d 2854	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴 ↑_o (𝐺‘suc 𝑦)) ·_o suc (𝐹‘(𝐺‘suc 𝑦))))
212	161, 211	sseldd 3918	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘suc 𝑦)))
213	212	exp32 420	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (suc 𝑦 ∈ dom 𝐺 → ((𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦)) → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘suc 𝑦)))))
214	213	a2d 29	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘suc 𝑦)))))
215	136, 214	syl5 34	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘suc 𝑦)))))
216	215	expcom 413	. . . . . . 7 ⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_o suc (𝐺‘suc 𝑦))))))
217	80, 89, 98, 131, 216	finds2 7721	. . . . . 6 ⊢ (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥)))))
218	70, 71, 58, 217	syl3c 66	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_o suc (𝐺‘𝑥)))
219	69, 218	eqeltrd 2839	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘𝐾) ∈ (𝐴 ↑_o suc (𝐺‘𝑥)))
220	68, 219	sseldd 3918	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘𝐾) ∈ (𝐴 ↑_o 𝐶))
221	220	rexlimdvaa 3213	. 2 ⊢ (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻‘𝐾) ∈ (𝐴 ↑_o 𝐶)))
222		peano2 7711	. . . . 5 ⊢ (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
223	170, 222	simpl2im 503	. . . 4 ⊢ (𝜑 → suc dom 𝐺 ∈ ω)
224		elnn 7698	. . . 4 ⊢ ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
225	23, 223, 224	syl2anc 583	. . 3 ⊢ (𝜑 → 𝐾 ∈ ω)
226		nn0suc 7716	. . 3 ⊢ (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
227	225, 226	syl 17	. 2 ⊢ (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
228	13, 221, 227	mpjaod 856	1 ⊢ (𝜑 → (𝐻‘𝐾) ∈ (𝐴 ↑_o 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 = wceq 1539 ∈ wcel 2108 ∃wrex 3064 Vcvv 3422 ⊆ wss 3883 ∅c0 4253 class class class wbr 5070 Tr wtr 5187 E cep 5485 We wwe 5534 dom cdm 5580 “ cima 5583 Ord word 6250 Oncon0 6251 suc csuc 6253 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 Isom wiso 6419 (class class class)co 7255 ∈ cmpo 7257 ωcom 7687 supp csupp 7948 seq_ωcseqom 8248 +_o coa 8264 ·_o comu 8265 ↑_o coe 8266 finSupp cfsupp 9058 OrdIsocoi 9198 CNF ccnf 9349

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-seqom 8249 df-1o 8267 df-2o 8268 df-oadd 8271 df-omul 8272 df-oexp 8273 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-oi 9199 df-cnf 9350

This theorem is referenced by: cantnflt2 9361 cnfcomlem 9387

W3C validator