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

Theorem cantnflt 8554
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.
StepHypRef Expression
1 cantnfs.a . . . 4 (𝜑𝐴 ∈ On)
2 cantnflt.c . . . 4 (𝜑𝐶 ∈ On)
3 cantnflt.a . . . 4 (𝜑 → ∅ ∈ 𝐴)
4 oen0 7651 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝐶))
51, 2, 3, 4syl21anc 1323 . . 3 (𝜑 → ∅ ∈ (𝐴𝑜 𝐶))
6 fveq2 6178 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 4781 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐺𝑘)) ·𝑜 (𝐹‘(𝐺𝑘))) +𝑜 𝑧)), ∅)
98seqom0g 7536 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10syl6eq 2670 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2684 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴𝑜 𝐶) ↔ ∅ ∈ (𝐴𝑜 𝐶)))
135, 12syl5ibrcom 237 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴𝑜 𝐶)))
142adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 5721 . . . . . . 7 (𝐶 ∈ On → Ord 𝐶)
1614, 15syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → Ord 𝐶)
17 cantnflt.s . . . . . . . 8 (𝜑 → (𝐺𝐾) ⊆ 𝐶)
1817adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝐾) ⊆ 𝐶)
19 cantnfcl.g . . . . . . . . . 10 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 8420 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6032 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 8419 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 6999 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 220 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 5735 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 694 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 5800 . . . . . . . . . . 11 ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3028, 24, 29sylancl 693 . . . . . . . . . 10 (𝜑 → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3123, 30mpbird 247 . . . . . . . . 9 (𝜑𝐾 ⊆ dom 𝐺)
3231adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33 vex 3198 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 5792 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 795 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35syl5eleqr 2706 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 6481 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1324 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 3596 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7003 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 7293 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . . 14 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . . 15 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 8548 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 475 . . . . . . . . . . . 12 (𝜑𝐹:𝐵𝐴)
49 fdm 6038 . . . . . . . . . . . 12 (𝐹:𝐵𝐴 → dom 𝐹 = 𝐵)
5048, 49syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐵)
5142, 50syl5sseq 3645 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
52 onss 6975 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5345, 52syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5451, 53sstrd 3605 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5554adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5623adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5735, 56eqeltrrd 2700 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
58 ordsucelsuc 7007 . . . . . . . . . . 11 (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
5924, 58ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
6057, 59sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
6120ffvelrni 6344 . . . . . . . . 9 (𝑥 ∈ dom 𝐺 → (𝐺𝑥) ∈ (𝐹 supp ∅))
6260, 61syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐹 supp ∅))
6355, 62sseldd 3596 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ On)
64 suceloni 6998 . . . . . . 7 ((𝐺𝑥) ∈ On → suc (𝐺𝑥) ∈ On)
6563, 64syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ∈ On)
661adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
673adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
68 oewordi 7656 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶)))
6965, 14, 66, 67, 68syl31anc 1327 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶)))
7041, 69mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶))
7135fveq2d 6182 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
72 simprl 793 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
73 simpl 473 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
74 eleq1 2687 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
75 suceq 5778 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7675fveq2d 6182 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
77 fveq2 6178 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
78 suceq 5778 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7977, 78syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
8079oveq2d 6651 . . . . . . . . 9 (𝑥 = ∅ → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺‘∅)))
8176, 80eleq12d 2693 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅))))
8274, 81imbi12d 334 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅)))))
83 eleq1 2687 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
84 suceq 5778 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8584fveq2d 6182 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
86 fveq2 6178 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
87 suceq 5778 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8886, 87syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8988oveq2d 6651 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺𝑦)))
9085, 89eleq12d 2693 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))))
9183, 90imbi12d 334 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))))
92 eleq1 2687 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
93 suceq 5778 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9493fveq2d 6182 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
95 fveq2 6178 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
96 suceq 5778 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9795, 96syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9897oveq2d 6651 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺‘suc 𝑦)))
9994, 98eleq12d 2693 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦))))
10092, 99imbi12d 334 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))))
10148adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐹:𝐵𝐴)
10220ffvelrni 6344 . . . . . . . . . . . 12 (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
10351sselda 3595 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
104102, 103sylan2 491 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
105101, 104ffvelrnd 6346 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1061adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
107 onelon 5736 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
108106, 105, 107syl2anc 692 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10954sselda 3595 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
110102, 109sylan2 491 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
111 oecl 7602 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴𝑜 (𝐺‘∅)) ∈ On)
112106, 110, 111syl2anc 692 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴𝑜 (𝐺‘∅)) ∈ On)
1133adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
114 oen0 7651 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 (𝐺‘∅)))
115106, 110, 113, 114syl21anc 1323 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴𝑜 (𝐺‘∅)))
116 omord2 7632 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴𝑜 (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴)))
117108, 106, 112, 115, 116syl31anc 1327 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴)))
118105, 117mpbid 222 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
119 peano1 7070 . . . . . . . . . . . 12 ∅ ∈ ω
120119a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
12144, 1, 45, 19, 43, 8cantnfsuc 8552 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)))
122120, 121sylan2 491 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)))
12310oveq2i 6646 . . . . . . . . . . 11 (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅)
124 omcl 7601 . . . . . . . . . . . . 13 (((𝐴𝑜 (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
125112, 108, 124syl2anc 692 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
126 oa0 7581 . . . . . . . . . . . 12 (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
127125, 126syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
128123, 127syl5eq 2666 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
129122, 128eqtrd 2654 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
130 oesuc 7592 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴𝑜 suc (𝐺‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
131106, 110, 130syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴𝑜 suc (𝐺‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
132118, 129, 1313eltr4d 2714 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅)))
133132ex 450 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅))))
134 ordtr 5725 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13524, 134ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
136 trsuc 5798 . . . . . . . . . . 11 ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
137135, 136mpan 705 . . . . . . . . . 10 (suc 𝑦 ∈ dom 𝐺𝑦 ∈ dom 𝐺)
138137imim1i 63 . . . . . . . . 9 ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))))
1391ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐴 ∈ On)
140 eloni 5721 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → Ord 𝐴)
141139, 140syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → Ord 𝐴)
14248ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐹:𝐵𝐴)
14351ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
14420ffvelrni 6344 . . . . . . . . . . . . . . . . . 18 (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
145144ad2antrl 763 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
146143, 145sseldd 3596 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
147142, 146ffvelrnd 6346 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
148 ordsucss 7003 . . . . . . . . . . . . . . 15 (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
149141, 147, 148sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
150 onelon 5736 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151139, 147, 150syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
152 suceloni 6998 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
153151, 152syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
15454ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ On)
155154, 145sseldd 3596 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
156 oecl 7602 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On)
157139, 155, 156syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On)
158 omwordi 7636 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴)))
159153, 139, 157, 158syl3anc 1324 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴)))
160149, 159mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴))
161 oesuc 7592 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴))
162139, 155, 161syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴))
163160, 162sseqtr4d 3634 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴𝑜 suc (𝐺‘suc 𝑦)))
164 eloni 5721 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
165155, 164syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
166 vex 3198 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
167166sucid 5792 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
168166sucex 6996 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
169168epelc 5021 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
170167, 169mpbir 221 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
17145, 51ssexd 4796 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17244, 1, 45, 19, 43cantnfcl 8549 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
173172simpld 475 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17419oiiso 8427 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175171, 173, 174syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
176175ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
177137ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝑦 ∈ dom 𝐺)
178 simprl 793 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc 𝑦 ∈ dom 𝐺)
179 isorel 6561 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
180176, 177, 178, 179syl12anc 1322 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
181170, 180mpbii 223 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) E (𝐺‘suc 𝑦))
182 fvex 6188 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
183182epelc 5021 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
184181, 183sylib 208 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
185 ordsucss 7003 . . . . . . . . . . . . . . . . 17 (Ord (𝐺‘suc 𝑦) → ((𝐺𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)))
186165, 184, 185sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦))
18720ffvelrni 6344 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
188177, 187syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐹 supp ∅))
189154, 188sseldd 3596 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ On)
190 suceloni 6998 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) ∈ On → suc (𝐺𝑦) ∈ On)
191189, 190syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐺𝑦) ∈ On)
1923ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ∅ ∈ 𝐴)
193 oewordi 7656 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦))))
194191, 155, 139, 192, 193syl31anc 1327 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦))))
195186, 194mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦)))
196 simprr 795 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))
197195, 196sseldd 3596 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 (𝐺‘suc 𝑦)))
198 peano2 7071 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
199198ad2antlr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
2008cantnfvalf 8547 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
201200ffvelrni 6344 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
202199, 201syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
203 omcl 7601 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
204157, 151, 203syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
205 oaord 7612 . . . . . . . . . . . . . . 15 (((𝐻‘suc 𝑦) ∈ On ∧ (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On) → ((𝐻‘suc 𝑦) ∈ (𝐴𝑜 (𝐺‘suc 𝑦)) ↔ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦)))))
206202, 157, 204, 205syl3anc 1324 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐻‘suc 𝑦) ∈ (𝐴𝑜 (𝐺‘suc 𝑦)) ↔ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦)))))
207197, 206mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦))))
20844, 1, 45, 19, 43, 8cantnfsuc 8552 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)))
209198, 208sylan2 491 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)))
210209adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)))
211 omsuc 7591 . . . . . . . . . . . . . 14 (((𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦))))
212157, 151, 211syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦))))
213207, 210, 2123eltr4d 2714 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))))
214163, 213sseldd 3596 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))
215214exp32 630 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω) → (suc 𝑦 ∈ dom 𝐺 → ((𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)) → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))))
216215a2d 29 . . . . . . . . 9 ((𝜑𝑦 ∈ ω) → ((suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))))
217138, 216syl5 34 . . . . . . . 8 ((𝜑𝑦 ∈ ω) → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))))
218217expcom 451 . . . . . . 7 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦))))))
21982, 91, 100, 133, 218finds2 7079 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)))))
22072, 73, 60, 219syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)))
22171, 220eqeltrd 2699 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴𝑜 suc (𝐺𝑥)))
22270, 221sseldd 3596 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴𝑜 𝐶))
223222rexlimdvaa 3028 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴𝑜 𝐶)))
224172simprd 479 . . . . 5 (𝜑 → dom 𝐺 ∈ ω)
225 peano2 7071 . . . . 5 (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
226224, 225syl 17 . . . 4 (𝜑 → suc dom 𝐺 ∈ ω)
227 elnn 7060 . . . 4 ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
22823, 226, 227syl2anc 692 . . 3 (𝜑𝐾 ∈ ω)
229 nn0suc 7075 . . 3 (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
230228, 229syl 17 . 2 (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
23113, 223, 230mpjaod 396 1 (𝜑 → (𝐻𝐾) ∈ (𝐴𝑜 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1481  wcel 1988  wrex 2910  Vcvv 3195  wss 3567  c0 3907   class class class wbr 4644  Tr wtr 4743   E cep 5018   We wwe 5062  dom cdm 5104  cima 5107  Ord word 5710  Oncon0 5711  suc csuc 5713   Fn wfn 5871  wf 5872  cfv 5876   Isom wiso 5877  (class class class)co 6635  cmpt2 6637  ωcom 7050   supp csupp 7280  seq𝜔cseqom 7527   +𝑜 coa 7542   ·𝑜 comu 7543  𝑜 coe 7544   finSupp cfsupp 8260  OrdIsocoi 8399   CNF ccnf 8543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-seqom 7528  df-1o 7545  df-2o 7546  df-oadd 7549  df-omul 7550  df-oexp 7551  df-er 7727  df-map 7844  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-oi 8400  df-cnf 8544
This theorem is referenced by:  cantnflt2  8555  cnfcomlem  8581
  Copyright terms: Public domain W3C validator