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

Theorem cantnflt 8733
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 7820 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 𝐶))
51, 2, 3, 4syl21anc 1475 . . 3 (𝜑 → ∅ ∈ (𝐴𝑜 𝐶))
6 fveq2 6332 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 4924 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐺𝑘)) ·𝑜 (𝐹‘(𝐺𝑘))) +𝑜 𝑧)), ∅)
98seqom0g 7704 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10syl6eq 2821 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2835 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴𝑜 𝐶) ↔ ∅ ∈ (𝐴𝑜 𝐶)))
135, 12syl5ibrcom 237 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴𝑜 𝐶)))
142adantr 466 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 5876 . . . . . . 7 (𝐶 ∈ On → Ord 𝐶)
1614, 15syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → Ord 𝐶)
17 cantnflt.s . . . . . . . 8 (𝜑 → (𝐺𝐾) ⊆ 𝐶)
1817adantr 466 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝐾) ⊆ 𝐶)
19 cantnfcl.g . . . . . . . . . 10 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 8591 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6185 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 8590 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 7161 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 220 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 5890 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 575 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 5955 . . . . . . . . . . 11 ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3028, 24, 29sylancl 574 . . . . . . . . . 10 (𝜑 → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3123, 30mpbird 247 . . . . . . . . 9 (𝜑𝐾 ⊆ dom 𝐺)
3231adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33 vex 3354 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 5947 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 756 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35syl5eleqr 2857 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 6639 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1476 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 3753 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7165 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 7459 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . . 14 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . . 15 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 8727 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 482 . . . . . . . . . . . 12 (𝜑𝐹:𝐵𝐴)
49 fdm 6191 . . . . . . . . . . . 12 (𝐹:𝐵𝐴 → dom 𝐹 = 𝐵)
5048, 49syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐵)
5142, 50syl5sseq 3802 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
52 onss 7137 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5345, 52syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5451, 53sstrd 3762 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5554adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5623adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5735, 56eqeltrrd 2851 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
58 ordsucelsuc 7169 . . . . . . . . . . 11 (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
5924, 58ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
6057, 59sylibr 224 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
6120ffvelrni 6501 . . . . . . . . 9 (𝑥 ∈ dom 𝐺 → (𝐺𝑥) ∈ (𝐹 supp ∅))
6260, 61syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐹 supp ∅))
6355, 62sseldd 3753 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ On)
64 suceloni 7160 . . . . . . 7 ((𝐺𝑥) ∈ On → suc (𝐺𝑥) ∈ On)
6563, 64syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ∈ On)
661adantr 466 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
673adantr 466 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
68 oewordi 7825 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶)))
6965, 14, 66, 67, 68syl31anc 1479 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶)))
7041, 69mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴𝑜 suc (𝐺𝑥)) ⊆ (𝐴𝑜 𝐶))
7135fveq2d 6336 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
72 simprl 754 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
73 simpl 468 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
74 eleq1 2838 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
75 suceq 5933 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7675fveq2d 6336 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
77 fveq2 6332 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
78 suceq 5933 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7977, 78syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
8079oveq2d 6809 . . . . . . . . 9 (𝑥 = ∅ → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺‘∅)))
8176, 80eleq12d 2844 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅))))
8274, 81imbi12d 333 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅)))))
83 eleq1 2838 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
84 suceq 5933 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8584fveq2d 6336 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
86 fveq2 6332 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
87 suceq 5933 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8886, 87syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8988oveq2d 6809 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺𝑦)))
9085, 89eleq12d 2844 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))))
9183, 90imbi12d 333 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))))
92 eleq1 2838 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
93 suceq 5933 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9493fveq2d 6336 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
95 fveq2 6332 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
96 suceq 5933 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9795, 96syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9897oveq2d 6809 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴𝑜 suc (𝐺𝑥)) = (𝐴𝑜 suc (𝐺‘suc 𝑦)))
9994, 98eleq12d 2844 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)) ↔ (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦))))
10092, 99imbi12d 333 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))))
10148adantr 466 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐹:𝐵𝐴)
10220ffvelrni 6501 . . . . . . . . . . . 12 (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
10351sselda 3752 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
104102, 103sylan2 580 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
105101, 104ffvelrnd 6503 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1061adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
107 onelon 5891 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
108106, 105, 107syl2anc 573 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10954sselda 3752 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
110102, 109sylan2 580 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
111 oecl 7771 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴𝑜 (𝐺‘∅)) ∈ On)
112106, 110, 111syl2anc 573 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴𝑜 (𝐺‘∅)) ∈ On)
1133adantr 466 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
114 oen0 7820 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴𝑜 (𝐺‘∅)))
115106, 110, 113, 114syl21anc 1475 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴𝑜 (𝐺‘∅)))
116 omord2 7801 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴𝑜 (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴)))
117108, 106, 112, 115, 116syl31anc 1479 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴)))
118105, 117mpbid 222 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
119 peano1 7232 . . . . . . . . . . . 12 ∅ ∈ ω
120119a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
12144, 1, 45, 19, 43, 8cantnfsuc 8731 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)))
122120, 121sylan2 580 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)))
12310oveq2i 6804 . . . . . . . . . . 11 (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)) = (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅)
124 omcl 7770 . . . . . . . . . . . . 13 (((𝐴𝑜 (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
125112, 108, 124syl2anc 573 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On)
126 oa0 7750 . . . . . . . . . . . 12 (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
127125, 126syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
128123, 127syl5eq 2817 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))) +𝑜 (𝐻‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
129122, 128eqtrd 2805 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 (𝐹‘(𝐺‘∅))))
130 oesuc 7761 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴𝑜 suc (𝐺‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
131106, 110, 130syl2anc 573 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴𝑜 suc (𝐺‘∅)) = ((𝐴𝑜 (𝐺‘∅)) ·𝑜 𝐴))
132118, 129, 1313eltr4d 2865 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅)))
133132ex 397 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴𝑜 suc (𝐺‘∅))))
134 ordtr 5880 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13524, 134ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
136 trsuc 5953 . . . . . . . . . . 11 ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
137135, 136mpan 670 . . . . . . . . . 10 (suc 𝑦 ∈ dom 𝐺𝑦 ∈ dom 𝐺)
138137imim1i 63 . . . . . . . . 9 ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))))
1391ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐴 ∈ On)
140 eloni 5876 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → Ord 𝐴)
141139, 140syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → Ord 𝐴)
14248ad2antrr 705 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐹:𝐵𝐴)
14351ad2antrr 705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
14420ffvelrni 6501 . . . . . . . . . . . . . . . . . 18 (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
145144ad2antrl 707 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
146143, 145sseldd 3753 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
147142, 146ffvelrnd 6503 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
148 ordsucss 7165 . . . . . . . . . . . . . . 15 (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
149141, 147, 148sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
150 onelon 5891 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151139, 147, 150syl2anc 573 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
152 suceloni 7160 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
153151, 152syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
15454ad2antrr 705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ On)
155154, 145sseldd 3753 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
156 oecl 7771 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On)
157139, 155, 156syl2anc 573 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On)
158 omwordi 7805 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴)))
159153, 139, 157, 158syl3anc 1476 . . . . . . . . . . . . . 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 7761 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴))
162139, 155, 161syl2anc 573 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 suc (𝐺‘suc 𝑦)) = ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 𝐴))
163160, 162sseqtr4d 3791 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴𝑜 suc (𝐺‘suc 𝑦)))
164 eloni 5876 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
165155, 164syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
166 vex 3354 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
167166sucid 5947 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
168166sucex 7158 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
169168epelc 5164 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
170167, 169mpbir 221 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
17145, 51ssexd 4939 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17244, 1, 45, 19, 43cantnfcl 8728 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
173172simpld 482 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17419oiiso 8598 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175171, 173, 174syl2anc 573 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
176175ad2antrr 705 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
177137ad2antrl 707 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → 𝑦 ∈ dom 𝐺)
178 simprl 754 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc 𝑦 ∈ dom 𝐺)
179 isorel 6719 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
180176, 177, 178, 179syl12anc 1474 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
181170, 180mpbii 223 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) E (𝐺‘suc 𝑦))
182 fvex 6342 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
183182epelc 5164 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
184181, 183sylib 208 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
185 ordsucss 7165 . . . . . . . . . . . . . . . . 17 (Ord (𝐺‘suc 𝑦) → ((𝐺𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)))
186165, 184, 185sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦))
18720ffvelrni 6501 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
188177, 187syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐹 supp ∅))
189154, 188sseldd 3753 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐺𝑦) ∈ On)
190 suceloni 7160 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) ∈ On → suc (𝐺𝑦) ∈ On)
191189, 190syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc (𝐺𝑦) ∈ On)
1923ad2antrr 705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ∅ ∈ 𝐴)
193 oewordi 7825 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦))))
194191, 155, 139, 192, 193syl31anc 1479 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦))))
195186, 194mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐴𝑜 suc (𝐺𝑦)) ⊆ (𝐴𝑜 (𝐺‘suc 𝑦)))
196 simprr 756 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))
197195, 196sseldd 3753 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 (𝐺‘suc 𝑦)))
198 peano2 7233 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
199198ad2antlr 706 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
2008cantnfvalf 8726 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
201200ffvelrni 6501 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
202199, 201syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
203 omcl 7770 . . . . . . . . . . . . . . . 16 (((𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
204157, 151, 203syl2anc 573 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
205 oaord 7781 . . . . . . . . . . . . . . 15 (((𝐻‘suc 𝑦) ∈ On ∧ (𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) ∈ On) → ((𝐻‘suc 𝑦) ∈ (𝐴𝑜 (𝐺‘suc 𝑦)) ↔ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)) ∈ (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦)))))
206202, 157, 204, 205syl3anc 1476 . . . . . . . . . . . . . 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 8731 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)))
209198, 208sylan2 580 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)))
210209adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐻‘suc 𝑦)))
211 omsuc 7760 . . . . . . . . . . . . . 14 (((𝐴𝑜 (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦))))
212157, 151, 211syl2anc 573 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 (𝐹‘(𝐺‘suc 𝑦))) +𝑜 (𝐴𝑜 (𝐺‘suc 𝑦))))
213207, 210, 2123eltr4d 2865 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴𝑜 (𝐺‘suc 𝑦)) ·𝑜 suc (𝐹‘(𝐺‘suc 𝑦))))
214163, 213sseldd 3753 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦)))
215214exp32 407 . . . . . . . . . 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 398 . . . . . . 7 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴𝑜 suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴𝑜 suc (𝐺‘suc 𝑦))))))
21982, 91, 100, 133, 218finds2 7241 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)))))
22072, 73, 60, 219syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴𝑜 suc (𝐺𝑥)))
22171, 220eqeltrd 2850 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴𝑜 suc (𝐺𝑥)))
22270, 221sseldd 3753 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴𝑜 𝐶))
223222rexlimdvaa 3180 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴𝑜 𝐶)))
224172simprd 483 . . . . 5 (𝜑 → dom 𝐺 ∈ ω)
225 peano2 7233 . . . . 5 (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
226224, 225syl 17 . . . 4 (𝜑 → suc dom 𝐺 ∈ ω)
227 elnn 7222 . . . 4 ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
22823, 226, 227syl2anc 573 . . 3 (𝜑𝐾 ∈ ω)
229 nn0suc 7237 . . 3 (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
230228, 229syl 17 . 2 (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
23113, 223, 230mpjaod 849 1 (𝜑 → (𝐻𝐾) ∈ (𝐴𝑜 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 836   = wceq 1631  wcel 2145  wrex 3062  Vcvv 3351  wss 3723  c0 4063   class class class wbr 4786  Tr wtr 4886   E cep 5161   We wwe 5207  dom cdm 5249  cima 5252  Ord word 5865  Oncon0 5866  suc csuc 5868   Fn wfn 6026  wf 6027  cfv 6031   Isom wiso 6032  (class class class)co 6793  cmpt2 6795  ωcom 7212   supp csupp 7446  seq𝜔cseqom 7695   +𝑜 coa 7710   ·𝑜 comu 7711  𝑜 coe 7712   finSupp cfsupp 8431  OrdIsocoi 8570   CNF ccnf 8722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-seqom 7696  df-1o 7713  df-2o 7714  df-oadd 7717  df-omul 7718  df-oexp 7719  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-oi 8571  df-cnf 8723
This theorem is referenced by:  cantnflt2  8734  cnfcomlem  8760
  Copyright terms: Public domain W3C validator