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 8569

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 𝐴 ↑_𝑜 𝐶 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 ↦ (((𝐴 ↑_𝑜 (𝐺‘𝑘)) ·_𝑜 (𝐹‘(𝐺‘𝑘))) +_𝑜 𝑧)), ∅)
cantnflt.a	⊢ (𝜑 → ∅ ∈ 𝐴)
cantnflt.k	⊢ (𝜑 → 𝐾 ∈ suc dom 𝐺)
cantnflt.c	⊢ (𝜑 → 𝐶 ∈ On)
cantnflt.s	⊢ (𝜑 → (𝐺 “ 𝐾) ⊆ 𝐶)

**Assertion**
Ref	Expression
cantnflt	⊢ (𝜑 → (𝐻‘𝐾) ∈ (𝐴 ↑_𝑜 𝐶))

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 7666	. . . 4 ⊢ (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_𝑜 𝐶))
5	1, 2, 3, 4	syl21anc 1325	. . 3 ⊢ (𝜑 → ∅ ∈ (𝐴 ↑_𝑜 𝐶))
6		fveq2 6191	. . . . 5 ⊢ (𝐾 = ∅ → (𝐻‘𝐾) = (𝐻‘∅))
7		0ex 4790	. . . . . 6 ⊢ ∅ ∈ V
8		cantnfval.h	. . . . . . 7 ⊢ 𝐻 = seq_𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑_𝑜 (𝐺‘𝑘)) ·_𝑜 (𝐹‘(𝐺‘𝑘))) +_𝑜 𝑧)), ∅)
9	8	seqom0g 7551	. . . . . 6 ⊢ (∅ ∈ V → (𝐻‘∅) = ∅)
10	7, 9	ax-mp 5	. . . . 5 ⊢ (𝐻‘∅) = ∅
11	6, 10	syl6eq 2672	. . . 4 ⊢ (𝐾 = ∅ → (𝐻‘𝐾) = ∅)
12	11	eleq1d 2686	. . 3 ⊢ (𝐾 = ∅ → ((𝐻‘𝐾) ∈ (𝐴 ↑_𝑜 𝐶) ↔ ∅ ∈ (𝐴 ↑_𝑜 𝐶)))
13	5, 12	syl5ibrcom 237	. 2 ⊢ (𝜑 → (𝐾 = ∅ → (𝐻‘𝐾) ∈ (𝐴 ↑_𝑜 𝐶)))
14	2	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15		eloni 5733	. . . . . . 7 ⊢ (𝐶 ∈ On → Ord 𝐶)
16	14, 15	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → Ord 𝐶)
17		cantnflt.s	. . . . . . . 8 ⊢ (𝜑 → (𝐺 “ 𝐾) ⊆ 𝐶)
18	17	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺 “ 𝐾) ⊆ 𝐶)
19		cantnfcl.g	. . . . . . . . . 10 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
20	19	oif 8435	. . . . . . . . 9 ⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21		ffn 6045	. . . . . . . . 9 ⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
22	20, 21	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23		cantnflt.k	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ suc dom 𝐺)
24	19	oicl 8434	. . . . . . . . . . . . 13 ⊢ Ord dom 𝐺
25		ordsuc 7014	. . . . . . . . . . . . 13 ⊢ (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
26	24, 25	mpbi 220	. . . . . . . . . . . 12 ⊢ Ord suc dom 𝐺
27		ordelon 5747	. . . . . . . . . . . 12 ⊢ ((Ord suc dom 𝐺 ∧ 𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
28	26, 23, 27	sylancr 695	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ On)
29		ordsssuc 5812	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺 ↔ 𝐾 ∈ suc dom 𝐺))
30	28, 24, 29	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾 ⊆ dom 𝐺 ↔ 𝐾 ∈ suc dom 𝐺))
31	23, 30	mpbird 247	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ⊆ dom 𝐺)
32	31	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33		vex 3203	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
34	33	sucid 5804	. . . . . . . . 9 ⊢ 𝑥 ∈ suc 𝑥
35		simprr 796	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
36	34, 35	syl5eleqr 2708	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ 𝐾)
37		fnfvima 6496	. . . . . . . 8 ⊢ ((𝐺 Fn dom 𝐺 ∧ 𝐾 ⊆ dom 𝐺 ∧ 𝑥 ∈ 𝐾) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐾))
38	22, 32, 36, 37	syl3anc 1326	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐾))
39	18, 38	sseldd 3604	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ 𝐶)
40		ordsucss 7018	. . . . . 6 ⊢ (Ord 𝐶 → ((𝐺‘𝑥) ∈ 𝐶 → suc (𝐺‘𝑥) ⊆ 𝐶))
41	16, 39, 40	sylc 65	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺‘𝑥) ⊆ 𝐶)
42		suppssdm 7308	. . . . . . . . . . 11 ⊢ (𝐹 supp ∅) ⊆ dom 𝐹
43		cantnfcl.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
44		cantnfs.s	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = dom (𝐴 CNF 𝐵)
45		cantnfs.b	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ On)
46	44, 1, 45	cantnfs 8563	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
47	43, 46	mpbid 222	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
48	47	simpld 475	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐵⟶𝐴)
49		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝐹:𝐵⟶𝐴 → dom 𝐹 = 𝐵)
50	48, 49	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = 𝐵)
51	42, 50	syl5sseq 3653	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
52		onss 6990	. . . . . . . . . . 11 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
53	45, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ⊆ On)
54	51, 53	sstrd 3613	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ On)
55	54	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
56	23	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
57	35, 56	eqeltrrd 2702	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
58		ordsucelsuc 7022	. . . . . . . . . . 11 ⊢ (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
59	24, 58	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
60	57, 59	sylibr 224	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
61	20	ffvelrni 6358	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐺 → (𝐺‘𝑥) ∈ (𝐹 supp ∅))
62	60, 61	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ (𝐹 supp ∅))
63	55, 62	sseldd 3604	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺‘𝑥) ∈ On)
64		suceloni 7013	. . . . . . 7 ⊢ ((𝐺‘𝑥) ∈ On → suc (𝐺‘𝑥) ∈ On)
65	63, 64	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺‘𝑥) ∈ On)
66	1	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
67	3	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
68		oewordi 7671	. . . . . 6 ⊢ (((suc (𝐺‘𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺‘𝑥) ⊆ 𝐶 → (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) ⊆ (𝐴 ↑_𝑜 𝐶)))
69	65, 14, 66, 67, 68	syl31anc 1329	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺‘𝑥) ⊆ 𝐶 → (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) ⊆ (𝐴 ↑_𝑜 𝐶)))
70	41, 69	mpd 15	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) ⊆ (𝐴 ↑_𝑜 𝐶))
71	35	fveq2d 6195	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘𝐾) = (𝐻‘suc 𝑥))
72		simprl 794	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
73		simpl 473	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
74		eleq1 2689	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
75		suceq 5790	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → suc 𝑥 = suc ∅)
76	75	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
77		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝐺‘𝑥) = (𝐺‘∅))
78		suceq 5790	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑥) = (𝐺‘∅) → suc (𝐺‘𝑥) = suc (𝐺‘∅))
79	77, 78	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → suc (𝐺‘𝑥) = suc (𝐺‘∅))
80	79	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) = (𝐴 ↑_𝑜 suc (𝐺‘∅)))
81	76, 80	eleq12d 2695	. . . . . . . 8 ⊢ (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴 ↑_𝑜 suc (𝐺‘∅))))
82	74, 81	imbi12d 334	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴 ↑_𝑜 suc (𝐺‘∅)))))
83		eleq1 2689	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺 ↔ 𝑦 ∈ dom 𝐺))
84		suceq 5790	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
85	84	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
86		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝐺‘𝑥) = (𝐺‘𝑦))
87		suceq 5790	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑥) = (𝐺‘𝑦) → suc (𝐺‘𝑥) = suc (𝐺‘𝑦))
88	86, 87	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → suc (𝐺‘𝑥) = suc (𝐺‘𝑦))
89	88	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) = (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))
90	85, 89	eleq12d 2695	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦))))
91	83, 90	imbi12d 334	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))))
92		eleq1 2689	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
93		suceq 5790	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
94	93	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
95		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝐺‘𝑥) = (𝐺‘suc 𝑦))
96		suceq 5790	. . . . . . . . . . 11 ⊢ ((𝐺‘𝑥) = (𝐺‘suc 𝑦) → suc (𝐺‘𝑥) = suc (𝐺‘suc 𝑦))
97	95, 96	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → suc (𝐺‘𝑥) = suc (𝐺‘suc 𝑦))
98	97	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) = (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)))
99	94, 98	eleq12d 2695	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥)) ↔ (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦))))
100	92, 99	imbi12d 334	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)))))
101	48	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐹:𝐵⟶𝐴)
102	20	ffvelrni 6358	. . . . . . . . . . . 12 ⊢ (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
103	51	sselda 3603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
104	102, 103	sylan2 491	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
105	101, 104	ffvelrnd 6360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
106	1	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
107		onelon 5748	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
108	106, 105, 107	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
109	54	sselda 3603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
110	102, 109	sylan2 491	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
111		oecl 7617	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴 ↑_𝑜 (𝐺‘∅)) ∈ On)
112	106, 110, 111	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴 ↑_𝑜 (𝐺‘∅)) ∈ On)
113	3	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
114		oen0 7666	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ↑_𝑜 (𝐺‘∅)))
115	106, 110, 113, 114	syl21anc 1325	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴 ↑_𝑜 (𝐺‘∅)))
116		omord2 7647	. . . . . . . . . . 11 ⊢ ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ↑_𝑜 (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴 ↑_𝑜 (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 𝐴)))
117	108, 106, 112, 115, 116	syl31anc 1329	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 𝐴)))
118	105, 117	mpbid 222	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 𝐴))
119		peano1 7085	. . . . . . . . . . . 12 ⊢ ∅ ∈ ω
120	119	a1i 11	. . . . . . . . . . 11 ⊢ (∅ ∈ dom 𝐺 → ∅ ∈ ω)
121	44, 1, 45, 19, 43, 8	cantnfsuc 8567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) +_𝑜 (𝐻‘∅)))
122	120, 121	sylan2 491	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) +_𝑜 (𝐻‘∅)))
123	10	oveq2i 6661	. . . . . . . . . . 11 ⊢ (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) +_𝑜 (𝐻‘∅)) = (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) +_𝑜 ∅)
124		omcl 7616	. . . . . . . . . . . . 13 ⊢ (((𝐴 ↑_𝑜 (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
125	112, 108, 124	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
126		oa0 7596	. . . . . . . . . . . 12 ⊢ (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) +_𝑜 ∅) = ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))))
127	125, 126	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) +_𝑜 ∅) = ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))))
128	123, 127	syl5eq 2668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))) +_𝑜 (𝐻‘∅)) = ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))))
129	122, 128	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 (𝐹‘(𝐺‘∅))))
130		oesuc 7607	. . . . . . . . . 10 ⊢ ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴 ↑_𝑜 suc (𝐺‘∅)) = ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 𝐴))
131	106, 110, 130	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴 ↑_𝑜 suc (𝐺‘∅)) = ((𝐴 ↑_𝑜 (𝐺‘∅)) ·_𝑜 𝐴))
132	118, 129, 131	3eltr4d 2716	. . . . . . . 8 ⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴 ↑_𝑜 suc (𝐺‘∅)))
133	132	ex 450	. . . . . . 7 ⊢ (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴 ↑_𝑜 suc (𝐺‘∅))))
134		ordtr 5737	. . . . . . . . . . . 12 ⊢ (Ord dom 𝐺 → Tr dom 𝐺)
135	24, 134	ax-mp 5	. . . . . . . . . . 11 ⊢ Tr dom 𝐺
136		trsuc 5810	. . . . . . . . . . 11 ⊢ ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
137	135, 136	mpan 706	. . . . . . . . . 10 ⊢ (suc 𝑦 ∈ dom 𝐺 → 𝑦 ∈ dom 𝐺)
138	137	imim1i 63	. . . . . . . . 9 ⊢ ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦))))
139	1	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → 𝐴 ∈ On)
140		eloni 5733	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ On → Ord 𝐴)
141	139, 140	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → Ord 𝐴)
142	48	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → 𝐹:𝐵⟶𝐴)
143	51	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
144	20	ffvelrni 6358	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
145	144	ad2antrl 764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
146	143, 145	sseldd 3604	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
147	142, 146	ffvelrnd 6360	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
148		ordsucss 7018	. . . . . . . . . . . . . . 15 ⊢ (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
149	141, 147, 148	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
150		onelon 5748	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151	139, 147, 150	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
152		suceloni 7013	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
153	151, 152	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
154	54	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐹 supp ∅) ⊆ On)
155	154, 145	sseldd 3604	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
156		oecl 7617	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ∈ On)
157	139, 155, 156	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ∈ On)
158		omwordi 7651	. . . . . . . . . . . . . . 15 ⊢ ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 𝐴)))
159	153, 139, 157, 158	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 𝐴)))
160	149, 159	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 𝐴))
161		oesuc 7607	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 𝐴))
162	139, 155, 161	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 𝐴))
163	160, 162	sseqtr4d 3642	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)))
164		eloni 5733	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
165	155, 164	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → Ord (𝐺‘suc 𝑦))
166		vex 3203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑦 ∈ V
167	166	sucid 5804	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑦 ∈ suc 𝑦
168	166	sucex 7011	. . . . . . . . . . . . . . . . . . . . 21 ⊢ suc 𝑦 ∈ V
169	168	epelc 5031	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 E suc 𝑦 ↔ 𝑦 ∈ suc 𝑦)
170	167, 169	mpbir 221	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑦 E suc 𝑦
171	45, 51	ssexd 4805	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
172	44, 1, 45, 19, 43	cantnfcl 8564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
173	172	simpld 475	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → E We (𝐹 supp ∅))
174	19	oiiso 8442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175	171, 173, 174	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
176	175	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
177	137	ad2antrl 764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → 𝑦 ∈ dom 𝐺)
178		simprl 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → suc 𝑦 ∈ dom 𝐺)
179		isorel 6576	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺‘𝑦) E (𝐺‘suc 𝑦)))
180	176, 177, 178, 179	syl12anc 1324	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺‘𝑦) E (𝐺‘suc 𝑦)))
181	170, 180	mpbii 223	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐺‘𝑦) E (𝐺‘suc 𝑦))
182		fvex 6201	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺‘suc 𝑦) ∈ V
183	182	epelc 5031	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺‘𝑦) ∈ (𝐺‘suc 𝑦))
184	181, 183	sylib 208	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐺‘𝑦) ∈ (𝐺‘suc 𝑦))
185		ordsucss 7018	. . . . . . . . . . . . . . . . 17 ⊢ (Ord (𝐺‘suc 𝑦) → ((𝐺‘𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)))
186	165, 184, 185	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦))
187	20	ffvelrni 6358	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ dom 𝐺 → (𝐺‘𝑦) ∈ (𝐹 supp ∅))
188	177, 187	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐺‘𝑦) ∈ (𝐹 supp ∅))
189	154, 188	sseldd 3604	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐺‘𝑦) ∈ On)
190		suceloni 7013	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺‘𝑦) ∈ On → suc (𝐺‘𝑦) ∈ On)
191	189, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → suc (𝐺‘𝑦) ∈ On)
192	3	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → ∅ ∈ 𝐴)
193		oewordi 7671	. . . . . . . . . . . . . . . . 17 ⊢ (((suc (𝐺‘𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴 ↑_𝑜 suc (𝐺‘𝑦)) ⊆ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦))))
194	191, 155, 139, 192, 193	syl31anc 1329	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴 ↑_𝑜 suc (𝐺‘𝑦)) ⊆ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦))))
195	186, 194	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐴 ↑_𝑜 suc (𝐺‘𝑦)) ⊆ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)))
196		simprr 796	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))
197	195, 196	sseldd 3604	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)))
198		peano2 7086	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
199	198	ad2antlr 763	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → suc 𝑦 ∈ ω)
200	8	cantnfvalf 8562	. . . . . . . . . . . . . . . . 17 ⊢ 𝐻:ω⟶On
201	200	ffvelrni 6358	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
202	199, 201	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
203		omcl 7616	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
204	157, 151, 203	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
205		oaord 7627	. . . . . . . . . . . . . . 15 ⊢ (((𝐻‘suc 𝑦) ∈ On ∧ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On) → ((𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ↔ (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)))))
206	202, 157, 204, 205	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → ((𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ↔ (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐴 ↑_𝑜 (𝐺‘suc 𝑦)))))
207	197, 206	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐴 ↑_𝑜 (𝐺‘suc 𝑦))))
208	44, 1, 45, 19, 43, 8	cantnfsuc 8567	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐻‘suc 𝑦)))
209	198, 208	sylan2 491	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐻‘suc 𝑦)))
210	209	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐻‘suc suc 𝑦) = (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐻‘suc 𝑦)))
211		omsuc 7606	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐴 ↑_𝑜 (𝐺‘suc 𝑦))))
212	157, 151, 211	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 (𝐹‘(𝐺‘suc 𝑦))) +_𝑜 (𝐴 ↑_𝑜 (𝐺‘suc 𝑦))))
213	207, 210, 212	3eltr4d 2716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴 ↑_𝑜 (𝐺‘suc 𝑦)) ·_𝑜 suc (𝐹‘(𝐺‘suc 𝑦))))
214	163, 213	sseldd 3604	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)))
215	214	exp32 631	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (suc 𝑦 ∈ dom 𝐺 → ((𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦)) → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)))))
216	215	a2d 29	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)))))
217	138, 216	syl5 34	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦)))))
218	217	expcom 451	. . . . . . 7 ⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴 ↑_𝑜 suc (𝐺‘suc 𝑦))))))
219	82, 91, 100, 133, 218	finds2 7094	. . . . . 6 ⊢ (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥)))))
220	72, 73, 60, 219	syl3c 66	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥)))
221	71, 220	eqeltrd 2701	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘𝐾) ∈ (𝐴 ↑_𝑜 suc (𝐺‘𝑥)))
222	70, 221	sseldd 3604	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘𝐾) ∈ (𝐴 ↑_𝑜 𝐶))
223	222	rexlimdvaa 3032	. 2 ⊢ (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻‘𝐾) ∈ (𝐴 ↑_𝑜 𝐶)))
224	172	simprd 479	. . . . 5 ⊢ (𝜑 → dom 𝐺 ∈ ω)
225		peano2 7086	. . . . 5 ⊢ (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
226	224, 225	syl 17	. . . 4 ⊢ (𝜑 → suc dom 𝐺 ∈ ω)
227		elnn 7075	. . . 4 ⊢ ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
228	23, 226, 227	syl2anc 693	. . 3 ⊢ (𝜑 → 𝐾 ∈ ω)
229		nn0suc 7090	. . 3 ⊢ (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
230	228, 229	syl 17	. 2 ⊢ (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
231	13, 223, 230	mpjaod 396	1 ⊢ (𝜑 → (𝐻‘𝐾) ∈ (𝐴 ↑_𝑜 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∃wrex 2913 Vcvv 3200 ⊆ wss 3574 ∅c0 3915 class class class wbr 4653 Tr wtr 4752 E cep 5028 We wwe 5072 dom cdm 5114 “ cima 5117 Ord word 5722 Oncon0 5723 suc csuc 5725 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 Isom wiso 5889 (class class class)co 6650 ↦ cmpt2 6652 ωcom 7065 supp csupp 7295 seq_𝜔cseqom 7542 +_𝑜 coa 7557 ·_𝑜 comu 7558 ↑_𝑜 coe 7559 finSupp cfsupp 8275 OrdIsocoi 8414 CNF ccnf 8558

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-seqom 7543 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-oexp 7566 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-oi 8415 df-cnf 8559

This theorem is referenced by: cantnflt2 8570 cnfcomlem 8596

W3C validator