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