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

Theorem cantnflt 8566
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 7663 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝐶))
51, 2, 3, 4syl21anc 1324 . . 3 (𝜑 → ∅ ∈ (𝐴𝑜 𝐶))
6 fveq2 6189 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 4788 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐺𝑘)) ·𝑜 (𝐹‘(𝐺𝑘))) +𝑜 𝑧)), ∅)
98seqom0g 7548 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10syl6eq 2671 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2685 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴𝑜 𝐶) ↔ ∅ ∈ (𝐴𝑜 𝐶)))
135, 12syl5ibrcom 237 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴𝑜 𝐶)))
142adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 5731 . . . . . . 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 8432 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6043 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 8431 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 7011 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 220 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 5745 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 695 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 5810 . . . . . . . . . . 11 ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3028, 24, 29sylancl 694 . . . . . . . . . 10 (𝜑 → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3123, 30mpbird 247 . . . . . . . . 9 (𝜑𝐾 ⊆ dom 𝐺)
3231adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33 vex 3201 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 5802 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 796 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35syl5eleqr 2707 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 6493 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1325 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 3602 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7015 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 7305 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . . 14 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . . 15 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 8560 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 475 . . . . . . . . . . . 12 (𝜑𝐹:𝐵𝐴)
49 fdm 6049 . . . . . . . . . . . 12 (𝐹:𝐵𝐴 → dom 𝐹 = 𝐵)
5048, 49syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐵)
5142, 50syl5sseq 3651 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
52 onss 6987 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5345, 52syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5451, 53sstrd 3611 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5554adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5623adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5735, 56eqeltrrd 2701 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
58 ordsucelsuc 7019 . . . . . . . . . . 11 (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
5924, 58ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
6057, 59sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
6120ffvelrni 6356 . . . . . . . . 9 (𝑥 ∈ dom 𝐺 → (𝐺𝑥) ∈ (𝐹 supp ∅))
6260, 61syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐹 supp ∅))
6355, 62sseldd 3602 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ On)
64 suceloni 7010 . . . . . . 7 ((𝐺𝑥) ∈ On → suc (𝐺𝑥) ∈ On)
6563, 64syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ∈ On)
661adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
673adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
68 oewordi 7668 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶)))
6965, 14, 66, 67, 68syl31anc 1328 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶)))
7041, 69mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶))
7135fveq2d 6193 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
72 simprl 794 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
73 simpl 473 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
74 eleq1 2688 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
75 suceq 5788 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7675fveq2d 6193 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
77 fveq2 6189 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
78 suceq 5788 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7977, 78syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
8079oveq2d 6663 . . . . . . . . 9 (𝑥 = ∅ → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺‘∅)))
8176, 80eleq12d 2694 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅))))
8274, 81imbi12d 334 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅)))))
83 eleq1 2688 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
84 suceq 5788 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8584fveq2d 6193 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
86 fveq2 6189 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
87 suceq 5788 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8886, 87syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8988oveq2d 6663 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺𝑦)))
9085, 89eleq12d 2694 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))))
9183, 90imbi12d 334 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))))
92 eleq1 2688 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
93 suceq 5788 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9493fveq2d 6193 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
95 fveq2 6189 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
96 suceq 5788 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9795, 96syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9897oveq2d 6663 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺‘suc 𝑦)))
9994, 98eleq12d 2694 . . . . . . . 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 6356 . . . . . . . . . . . 12 (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
10351sselda 3601 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
104102, 103sylan2 491 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
105101, 104ffvelrnd 6358 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1061adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
107 onelon 5746 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
108106, 105, 107syl2anc 693 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10954sselda 3601 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
110102, 109sylan2 491 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
111 oecl 7614 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴𝑜 (𝐺‘∅)) ∈ On)
112106, 110, 111syl2anc 693 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴𝑜 (𝐺‘∅)) ∈ On)
1133adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
114 oen0 7663 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 (𝐺‘∅)))
115106, 110, 113, 114syl21anc 1324 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴𝑜 (𝐺‘∅)))
116 omord2 7644 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴𝑜 (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴)))
117108, 106, 112, 115, 116syl31anc 1328 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴)))
118105, 117mpbid 222 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
119 peano1 7082 . . . . . . . . . . . 12 ∅ ∈ ω
120119a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
12144, 1, 45, 19, 43, 8cantnfsuc 8564 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)))
122120, 121sylan2 491 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)))
12310oveq2i 6658 . . . . . . . . . . 11 (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅)
124 omcl 7613 . . . . . . . . . . . . 13 (((𝐴𝑜 (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
125112, 108, 124syl2anc 693 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
126 oa0 7593 . . . . . . . . . . . 12 (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
127125, 126syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
128123, 127syl5eq 2667 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
129122, 128eqtrd 2655 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
130 oesuc 7604 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴𝑜 suc (𝐺‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
131106, 110, 130syl2anc 693 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴𝑜 suc (𝐺‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
132118, 129, 1313eltr4d 2715 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅)))
133132ex 450 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅))))
134 ordtr 5735 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13524, 134ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
136 trsuc 5808 . . . . . . . . . . 11 ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
137135, 136mpan 706 . . . . . . . . . 10 (suc 𝑦 ∈ dom 𝐺𝑦 ∈ dom 𝐺)
138137imim1i 63 . . . . . . . . 9 ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))))
1391ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐴 ∈ On)
140 eloni 5731 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → Ord 𝐴)
141139, 140syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → Ord 𝐴)
14248ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐹:𝐵𝐴)
14351ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
14420ffvelrni 6356 . . . . . . . . . . . . . . . . . 18 (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
145144ad2antrl 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
146143, 145sseldd 3602 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
147142, 146ffvelrnd 6358 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
148 ordsucss 7015 . . . . . . . . . . . . . . 15 (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
149141, 147, 148sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
150 onelon 5746 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151139, 147, 150syl2anc 693 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
152 suceloni 7010 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
153151, 152syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
15454ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ On)
155154, 145sseldd 3602 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
156 oecl 7614 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On)
157139, 155, 156syl2anc 693 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On)
158 omwordi 7648 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴)))
159153, 139, 157, 158syl3anc 1325 . . . . . . . . . . . . . 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 7604 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴))
162139, 155, 161syl2anc 693 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴))
163160, 162sseqtr4d 3640 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴𝑜 suc (𝐺‘suc 𝑦)))
164 eloni 5731 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
165155, 164syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
166 vex 3201 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
167166sucid 5802 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
168166sucex 7008 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
169168epelc 5029 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
170167, 169mpbir 221 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
17145, 51ssexd 4803 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17244, 1, 45, 19, 43cantnfcl 8561 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
173172simpld 475 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17419oiiso 8439 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175171, 173, 174syl2anc 693 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
176175ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
177137ad2antrl 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝑦 ∈ dom 𝐺)
178 simprl 794 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc 𝑦 ∈ dom 𝐺)
179 isorel 6573 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
180176, 177, 178, 179syl12anc 1323 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
181170, 180mpbii 223 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) E (𝐺‘suc 𝑦))
182 fvex 6199 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
183182epelc 5029 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
184181, 183sylib 208 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
185 ordsucss 7015 . . . . . . . . . . . . . . . . 17 (Ord (𝐺‘suc 𝑦) → ((𝐺𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)))
186165, 184, 185sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦))
18720ffvelrni 6356 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
188177, 187syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐹 supp ∅))
189154, 188sseldd 3602 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ On)
190 suceloni 7010 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) ∈ On → suc (𝐺𝑦) ∈ On)
191189, 190syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐺𝑦) ∈ On)
1923ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ∅ ∈ 𝐴)
193 oewordi 7668 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦))))
194191, 155, 139, 192, 193syl31anc 1328 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦))))
195186, 194mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦)))
196 simprr 796 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))
197195, 196sseldd 3602 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 (𝐺‘suc 𝑦)))
198 peano2 7083 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
199198ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
2008cantnfvalf 8559 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
201200ffvelrni 6356 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
202199, 201syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
203 omcl 7613 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
204157, 151, 203syl2anc 693 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
205 oaord 7624 . . . . . . . . . . . . . . 15 (((𝐻‘suc 𝑦) ∈ On ∧ (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On) → ((𝐻‘suc 𝑦) ∈ (𝐴𝑜 (𝐺‘suc 𝑦)) ↔ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦)))))
206202, 157, 204, 205syl3anc 1325 . . . . . . . . . . . . . 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 8564 . . . . . . . . . . . . . . 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 7603 . . . . . . . . . . . . . 14 (((𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦))))
212157, 151, 211syl2anc 693 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦))))
213207, 210, 2123eltr4d 2715 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))))
214163, 213sseldd 3602 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))
215214exp32 631 . . . . . . . . . 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 7091 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)))))
22072, 73, 60, 219syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)))
22171, 220eqeltrd 2700 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴𝑜 suc (𝐺𝑥)))
22270, 221sseldd 3602 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴𝑜 𝐶))
223222rexlimdvaa 3030 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴𝑜 𝐶)))
224172simprd 479 . . . . 5 (𝜑 → dom 𝐺 ∈ ω)
225 peano2 7083 . . . . 5 (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
226224, 225syl 17 . . . 4 (𝜑 → suc dom 𝐺 ∈ ω)
227 elnn 7072 . . . 4 ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
22823, 226, 227syl2anc 693 . . 3 (𝜑𝐾 ∈ ω)
229 nn0suc 7087 . . 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 1482  wcel 1989  wrex 2912  Vcvv 3198  wss 3572  c0 3913   class class class wbr 4651  Tr wtr 4750   E cep 5026   We wwe 5070  dom cdm 5112  cima 5115  Ord word 5720  Oncon0 5721  suc csuc 5723   Fn wfn 5881  wf 5882  cfv 5886   Isom wiso 5887  (class class class)co 6647  cmpt2 6649  ωcom 7062   supp csupp 7292  seq𝜔cseqom 7539   +𝑜 coa 7554   ·𝑜 comu 7555  𝑜 coe 7556   finSupp cfsupp 8272  OrdIsocoi 8411   CNF ccnf 8555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-supp 7293  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-seqom 7540  df-1o 7557  df-2o 7558  df-oadd 7561  df-omul 7562  df-oexp 7563  df-er 7739  df-map 7856  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-fsupp 8273  df-oi 8412  df-cnf 8556
This theorem is referenced by:  cantnflt2  8567  cnfcomlem  8593
  Copyright terms: Public domain W3C validator