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

Theorem cantnflt 9741
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 𝐴o 𝐶 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 ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
cantnflt.a (𝜑 → ∅ ∈ 𝐴)
cantnflt.k (𝜑𝐾 ∈ suc dom 𝐺)
cantnflt.c (𝜑𝐶 ∈ On)
cantnflt.s (𝜑 → (𝐺𝐾) ⊆ 𝐶)
Assertion
Ref Expression
cantnflt (𝜑 → (𝐻𝐾) ∈ (𝐴o 𝐶))
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 8642 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
51, 2, 3, 4syl21anc 837 . . 3 (𝜑 → ∅ ∈ (𝐴o 𝐶))
6 fveq2 6920 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 5325 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
98seqom0g 8512 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10eqtrdi 2796 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2829 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴o 𝐶) ↔ ∅ ∈ (𝐴o 𝐶)))
135, 12syl5ibrcom 247 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴o 𝐶)))
142adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 6405 . . . . . . 7 (𝐶 ∈ On → Ord 𝐶)
1614, 15syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → Ord 𝐶)
17 cantnflt.s . . . . . . . 8 (𝜑 → (𝐺𝐾) ⊆ 𝐶)
1817adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝐾) ⊆ 𝐶)
19 cantnfcl.g . . . . . . . . . 10 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 9599 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6747 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 9598 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 7849 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 230 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 6419 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 586 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 6484 . . . . . . . . . . 11 ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3028, 24, 29sylancl 585 . . . . . . . . . 10 (𝜑 → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3123, 30mpbird 257 . . . . . . . . 9 (𝜑𝐾 ⊆ dom 𝐺)
3231adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33 vex 3492 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 6477 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 772 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35eleqtrrid 2851 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 7270 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1371 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 4009 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7854 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 8218 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . 13 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . 14 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 9735 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 232 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 494 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝐴)
4942, 48fssdm 6766 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
50 onss 7820 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5145, 50syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5249, 51sstrd 4019 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5352adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5423adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5535, 54eqeltrrd 2845 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
56 ordsucelsuc 7858 . . . . . . . . . . 11 (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
5724, 56ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
5855, 57sylibr 234 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
5920ffvelcdmi 7117 . . . . . . . . 9 (𝑥 ∈ dom 𝐺 → (𝐺𝑥) ∈ (𝐹 supp ∅))
6058, 59syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐹 supp ∅))
6153, 60sseldd 4009 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ On)
62 onsuc 7847 . . . . . . 7 ((𝐺𝑥) ∈ On → suc (𝐺𝑥) ∈ On)
6361, 62syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ∈ On)
641adantr 480 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
653adantr 480 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
66 oewordi 8647 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6763, 14, 64, 65, 66syl31anc 1373 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6841, 67mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶))
6935fveq2d 6924 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
70 simprl 770 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
71 simpl 482 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
72 eleq1 2832 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
73 suceq 6461 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7473fveq2d 6924 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
75 fveq2 6920 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
76 suceq 6461 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7775, 76syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
7877oveq2d 7464 . . . . . . . . 9 (𝑥 = ∅ → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘∅)))
7974, 78eleq12d 2838 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
8072, 79imbi12d 344 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))))
81 eleq1 2832 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
82 suceq 6461 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8382fveq2d 6924 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
84 fveq2 6920 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
85 suceq 6461 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8684, 85syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8786oveq2d 7464 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺𝑦)))
8883, 87eleq12d 2838 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
8981, 88imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))))
90 eleq1 2832 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
91 suceq 6461 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9291fveq2d 6924 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
93 fveq2 6920 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
94 suceq 6461 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9593, 94syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9695oveq2d 7464 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘suc 𝑦)))
9792, 96eleq12d 2838 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦))))
9890, 97imbi12d 344 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))))
9948adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐹:𝐵𝐴)
10020ffvelcdmi 7117 . . . . . . . . . . . 12 (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
10149sselda 4008 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
102100, 101sylan2 592 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
10399, 102ffvelcdmd 7119 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1041adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
105 onelon 6420 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
106104, 103, 105syl2anc 583 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10752sselda 4008 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
108100, 107sylan2 592 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
109 oecl 8593 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o (𝐺‘∅)) ∈ On)
110104, 108, 109syl2anc 583 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o (𝐺‘∅)) ∈ On)
1113adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
112 oen0 8642 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o (𝐺‘∅)))
113104, 108, 111, 112syl21anc 837 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴o (𝐺‘∅)))
114 omord2 8623 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴o (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
115106, 104, 110, 113, 114syl31anc 1373 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
116103, 115mpbid 232 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴))
117 peano1 7927 . . . . . . . . . . . 12 ∅ ∈ ω
118117a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
11944, 1, 45, 19, 43, 8cantnfsuc 9739 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
120118, 119sylan2 592 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
12110oveq2i 7459 . . . . . . . . . . 11 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅)
122 omcl 8592 . . . . . . . . . . . . 13 (((𝐴o (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
123110, 106, 122syl2anc 583 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
124 oa0 8572 . . . . . . . . . . . 12 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
125123, 124syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
126121, 125eqtrid 2792 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
127120, 126eqtrd 2780 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
128 oesuc 8583 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
129104, 108, 128syl2anc 583 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
130116, 127, 1293eltr4d 2859 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))
131130ex 412 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
132 ordtr 6409 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13324, 132ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
134 trsuc 6482 . . . . . . . . . . 11 ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
135133, 134mpan 689 . . . . . . . . . 10 (suc 𝑦 ∈ dom 𝐺𝑦 ∈ dom 𝐺)
136135imim1i 63 . . . . . . . . 9 ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
1371ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐴 ∈ On)
138 eloni 6405 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → Ord 𝐴)
139137, 138syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord 𝐴)
14048ad2antrr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐹:𝐵𝐴)
14149ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
14220ffvelcdmi 7117 . . . . . . . . . . . . . . . . . 18 (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
143142ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
144141, 143sseldd 4009 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
145140, 144ffvelcdmd 7119 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
146 ordsucss 7854 . . . . . . . . . . . . . . 15 (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
147139, 145, 146sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
148 onelon 6420 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
149137, 145, 148syl2anc 583 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
150 onsuc 7847 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151149, 150syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
15252ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ On)
153152, 143sseldd 4009 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
154 oecl 8593 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
155137, 153, 154syl2anc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
156 omwordi 8627 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴)))
157151, 137, 155, 156syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴)))
158147, 157mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴))
159 oesuc 8583 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o suc (𝐺‘suc 𝑦)) = ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴))
160137, 153, 159syl2anc 583 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o suc (𝐺‘suc 𝑦)) = ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴))
161158, 160sseqtrrd 4050 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴o suc (𝐺‘suc 𝑦)))
162 eloni 6405 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
163153, 162syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
164 vex 3492 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
165164sucid 6477 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
166164sucex 7842 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
167166epeli 5601 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
168165, 167mpbir 231 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
169 ovexd 7483 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17044, 1, 45, 19, 43cantnfcl 9736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
171170simpld 494 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17219oiiso 9606 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
173169, 171, 172syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
174173ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175135ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝑦 ∈ dom 𝐺)
176 simprl 770 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ dom 𝐺)
177 isorel 7362 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
178174, 175, 176, 177syl12anc 836 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
179168, 178mpbii 233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) E (𝐺‘suc 𝑦))
180 fvex 6933 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
181180epeli 5601 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
182179, 181sylib 218 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
183 ordsucss 7854 . . . . . . . . . . . . . . . . 17 (Ord (𝐺‘suc 𝑦) → ((𝐺𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)))
184163, 182, 183sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦))
18520ffvelcdmi 7117 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
186175, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐹 supp ∅))
187152, 186sseldd 4009 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ On)
188 onsuc 7847 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) ∈ On → suc (𝐺𝑦) ∈ On)
189187, 188syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ∈ On)
1903ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ∅ ∈ 𝐴)
191 oewordi 8647 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴o suc (𝐺𝑦)) ⊆ (𝐴o (𝐺‘suc 𝑦))))
192189, 153, 137, 190, 191syl31anc 1373 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴o suc (𝐺𝑦)) ⊆ (𝐴o (𝐺‘suc 𝑦))))
193184, 192mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o suc (𝐺𝑦)) ⊆ (𝐴o (𝐺‘suc 𝑦)))
194 simprr 772 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))
195193, 194sseldd 4009 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)))
196 peano2 7929 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
197196ad2antlr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
1988cantnfvalf 9734 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
199198ffvelcdmi 7117 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
200197, 199syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
201 omcl 8592 . . . . . . . . . . . . . . . 16 (((𝐴o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
202155, 149, 201syl2anc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
203 oaord 8603 . . . . . . . . . . . . . . 15 (((𝐻‘suc 𝑦) ∈ On ∧ (𝐴o (𝐺‘suc 𝑦)) ∈ On ∧ ((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) ∈ On) → ((𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)) ↔ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)) ∈ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦)))))
204200, 155, 202, 203syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)) ↔ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)) ∈ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦)))))
205195, 204mpbid 232 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)) ∈ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦))))
20644, 1, 45, 19, 43, 8cantnfsuc 9739 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
207196, 206sylan2 592 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
208207adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
209 omsuc 8582 . . . . . . . . . . . . . 14 (((𝐴o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦))))
210155, 149, 209syl2anc 583 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦))))
211205, 208, 2103eltr4d 2859 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))))
212161, 211sseldd 4009 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))
213212exp32 420 . . . . . . . . . 10 ((𝜑𝑦 ∈ ω) → (suc 𝑦 ∈ dom 𝐺 → ((𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)) → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))))
214213a2d 29 . . . . . . . . 9 ((𝜑𝑦 ∈ ω) → ((suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))))
215136, 214syl5 34 . . . . . . . 8 ((𝜑𝑦 ∈ ω) → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))))
216215expcom 413 . . . . . . 7 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦))))))
21780, 89, 98, 131, 216finds2 7938 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))))
21870, 71, 58, 217syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))
21969, 218eqeltrd 2844 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o suc (𝐺𝑥)))
22068, 219sseldd 4009 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o 𝐶))
221220rexlimdvaa 3162 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴o 𝐶)))
222 peano2 7929 . . . . 5 (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
223170, 222simpl2im 503 . . . 4 (𝜑 → suc dom 𝐺 ∈ ω)
224 elnn 7914 . . . 4 ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
22523, 223, 224syl2anc 583 . . 3 (𝜑𝐾 ∈ ω)
226 nn0suc 7934 . . 3 (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
227225, 226syl 17 . 2 (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
22813, 221, 227mpjaod 859 1 (𝜑 → (𝐻𝐾) ∈ (𝐴o 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 846   = wceq 1537  wcel 2108  wrex 3076  Vcvv 3488  wss 3976  c0 4352   class class class wbr 5166  Tr wtr 5283   E cep 5598   We wwe 5651  dom cdm 5700  cima 5703  Ord word 6394  Oncon0 6395  suc csuc 6397   Fn wfn 6568  wf 6569  cfv 6573   Isom wiso 6574  (class class class)co 7448  cmpo 7450  ωcom 7903   supp csupp 8201  seqωcseqom 8503   +o coa 8519   ·o comu 8520  o coe 8521   finSupp cfsupp 9431  OrdIsocoi 9578   CNF ccnf 9730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-supp 8202  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-seqom 8504  df-1o 8522  df-2o 8523  df-oadd 8526  df-omul 8527  df-oexp 8528  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fsupp 9432  df-oi 9579  df-cnf 9731
This theorem is referenced by:  cantnflt2  9742  cnfcomlem  9768
  Copyright terms: Public domain W3C validator