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

Theorem cantnflt 9113
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 8190 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
51, 2, 3, 4syl21anc 835 . . 3 (𝜑 → ∅ ∈ (𝐴o 𝐶))
6 fveq2 6646 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 5187 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
98seqom0g 8070 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10syl6eq 2871 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2895 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴o 𝐶) ↔ ∅ ∈ (𝐴o 𝐶)))
135, 12syl5ibrcom 249 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴o 𝐶)))
142adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 6177 . . . . . . 7 (𝐶 ∈ On → Ord 𝐶)
1614, 15syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → Ord 𝐶)
17 cantnflt.s . . . . . . . 8 (𝜑 → (𝐺𝐾) ⊆ 𝐶)
1817adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝐾) ⊆ 𝐶)
19 cantnfcl.g . . . . . . . . . 10 𝐺 = OrdIso( E , (𝐹 supp ∅))
2019oif 8972 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6490 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 8971 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 7507 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 232 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 6191 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 589 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 6253 . . . . . . . . . . 11 ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3028, 24, 29sylancl 588 . . . . . . . . . 10 (𝜑 → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3123, 30mpbird 259 . . . . . . . . 9 (𝜑𝐾 ⊆ dom 𝐺)
3231adantr 483 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33 vex 3476 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 6246 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 771 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35eleqtrrid 2918 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 6972 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1367 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 3947 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7511 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 7821 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . 13 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . 14 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 9107 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 234 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 497 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝐴)
4942, 48fssdm 6506 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
50 onss 7483 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5145, 50syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5249, 51sstrd 3956 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5352adantr 483 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5423adantr 483 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5535, 54eqeltrrd 2912 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
56 ordsucelsuc 7515 . . . . . . . . . . 11 (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
5724, 56ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
5855, 57sylibr 236 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
5920ffvelrni 6826 . . . . . . . . 9 (𝑥 ∈ dom 𝐺 → (𝐺𝑥) ∈ (𝐹 supp ∅))
6058, 59syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐹 supp ∅))
6153, 60sseldd 3947 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ On)
62 suceloni 7506 . . . . . . 7 ((𝐺𝑥) ∈ On → suc (𝐺𝑥) ∈ On)
6361, 62syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ∈ On)
641adantr 483 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
653adantr 483 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
66 oewordi 8195 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6763, 14, 64, 65, 66syl31anc 1369 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6841, 67mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶))
6935fveq2d 6650 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
70 simprl 769 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
71 simpl 485 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
72 eleq1 2898 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
73 suceq 6232 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7473fveq2d 6650 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
75 fveq2 6646 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
76 suceq 6232 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7775, 76syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
7877oveq2d 7149 . . . . . . . . 9 (𝑥 = ∅ → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘∅)))
7974, 78eleq12d 2905 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
8072, 79imbi12d 347 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))))
81 eleq1 2898 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
82 suceq 6232 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8382fveq2d 6650 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
84 fveq2 6646 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
85 suceq 6232 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8684, 85syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8786oveq2d 7149 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺𝑦)))
8883, 87eleq12d 2905 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
8981, 88imbi12d 347 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))))
90 eleq1 2898 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
91 suceq 6232 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9291fveq2d 6650 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
93 fveq2 6646 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
94 suceq 6232 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9593, 94syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9695oveq2d 7149 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘suc 𝑦)))
9792, 96eleq12d 2905 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦))))
9890, 97imbi12d 347 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))))
9948adantr 483 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐹:𝐵𝐴)
10020ffvelrni 6826 . . . . . . . . . . . 12 (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
10149sselda 3946 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
102100, 101sylan2 594 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
10399, 102ffvelrnd 6828 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1041adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
105 onelon 6192 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
106104, 103, 105syl2anc 586 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10752sselda 3946 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
108100, 107sylan2 594 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
109 oecl 8140 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o (𝐺‘∅)) ∈ On)
110104, 108, 109syl2anc 586 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o (𝐺‘∅)) ∈ On)
1113adantr 483 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
112 oen0 8190 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o (𝐺‘∅)))
113104, 108, 111, 112syl21anc 835 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴o (𝐺‘∅)))
114 omord2 8171 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴o (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
115106, 104, 110, 113, 114syl31anc 1369 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
116103, 115mpbid 234 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴))
117 peano1 7579 . . . . . . . . . . . 12 ∅ ∈ ω
118117a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
11944, 1, 45, 19, 43, 8cantnfsuc 9111 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
120118, 119sylan2 594 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
12110oveq2i 7144 . . . . . . . . . . 11 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅)
122 omcl 8139 . . . . . . . . . . . . 13 (((𝐴o (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
123110, 106, 122syl2anc 586 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
124 oa0 8119 . . . . . . . . . . . 12 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
125123, 124syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
126121, 125syl5eq 2867 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
127120, 126eqtrd 2855 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
128 oesuc 8130 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
129104, 108, 128syl2anc 586 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
130116, 127, 1293eltr4d 2926 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))
131130ex 415 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
132 ordtr 6181 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13324, 132ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
134 trsuc 6251 . . . . . . . . . . 11 ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
135133, 134mpan 688 . . . . . . . . . 10 (suc 𝑦 ∈ dom 𝐺𝑦 ∈ dom 𝐺)
136135imim1i 63 . . . . . . . . 9 ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
1371ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐴 ∈ On)
138 eloni 6177 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → Ord 𝐴)
139137, 138syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord 𝐴)
14048ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐹:𝐵𝐴)
14149ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
14220ffvelrni 6826 . . . . . . . . . . . . . . . . . 18 (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
143142ad2antrl 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
144141, 143sseldd 3947 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
145140, 144ffvelrnd 6828 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
146 ordsucss 7511 . . . . . . . . . . . . . . 15 (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
147139, 145, 146sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
148 onelon 6192 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
149137, 145, 148syl2anc 586 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
150 suceloni 7506 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151149, 150syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
15252ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ On)
153152, 143sseldd 3947 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
154 oecl 8140 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
155137, 153, 154syl2anc 586 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
156 omwordi 8175 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴)))
157151, 137, 155, 156syl3anc 1367 . . . . . . . . . . . . . 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 8130 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o suc (𝐺‘suc 𝑦)) = ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴))
160137, 153, 159syl2anc 586 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o suc (𝐺‘suc 𝑦)) = ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴))
161158, 160sseqtrrd 3987 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴o suc (𝐺‘suc 𝑦)))
162 eloni 6177 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
163153, 162syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
164 vex 3476 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
165164sucid 6246 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
166164sucex 7504 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
167166epeli 5444 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
168165, 167mpbir 233 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
169 ovexd 7168 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17044, 1, 45, 19, 43cantnfcl 9108 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
171170simpld 497 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17219oiiso 8979 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
173169, 171, 172syl2anc 586 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
174173ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175135ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝑦 ∈ dom 𝐺)
176 simprl 769 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ dom 𝐺)
177 isorel 7056 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
178174, 175, 176, 177syl12anc 834 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
179168, 178mpbii 235 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) E (𝐺‘suc 𝑦))
180 fvex 6659 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
181180epeli 5444 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
182179, 181sylib 220 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
183 ordsucss 7511 . . . . . . . . . . . . . . . . 17 (Ord (𝐺‘suc 𝑦) → ((𝐺𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)))
184163, 182, 183sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦))
18520ffvelrni 6826 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
186175, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐹 supp ∅))
187152, 186sseldd 3947 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ On)
188 suceloni 7506 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) ∈ On → suc (𝐺𝑦) ∈ On)
189187, 188syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ∈ On)
1903ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ∅ ∈ 𝐴)
191 oewordi 8195 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴o suc (𝐺𝑦)) ⊆ (𝐴o (𝐺‘suc 𝑦))))
192189, 153, 137, 190, 191syl31anc 1369 . . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))
195193, 194sseldd 3947 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)))
196 peano2 7580 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
197196ad2antlr 725 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
1988cantnfvalf 9106 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
199198ffvelrni 6826 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
200197, 199syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
201 omcl 8139 . . . . . . . . . . . . . . . 16 (((𝐴o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
202155, 149, 201syl2anc 586 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
203 oaord 8151 . . . . . . . . . . . . . . 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 1367 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)) ↔ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)) ∈ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦)))))
205195, 204mpbid 234 . . . . . . . . . . . . 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 9111 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
207196, 206sylan2 594 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
208207adantr 483 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
209 omsuc 8129 . . . . . . . . . . . . . 14 (((𝐴o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦))))
210155, 149, 209syl2anc 586 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦))))
211205, 208, 2103eltr4d 2926 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))))
212161, 211sseldd 3947 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))
213212exp32 423 . . . . . . . . . 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 416 . . . . . . 7 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦))))))
21780, 89, 98, 131, 216finds2 7588 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))))
21870, 71, 58, 217syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))
21969, 218eqeltrd 2911 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o suc (𝐺𝑥)))
22068, 219sseldd 3947 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o 𝐶))
221220rexlimdvaa 3272 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴o 𝐶)))
222 peano2 7580 . . . . 5 (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
223170, 222simpl2im 506 . . . 4 (𝜑 → suc dom 𝐺 ∈ ω)
224 elnn 7568 . . . 4 ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
22523, 223, 224syl2anc 586 . . 3 (𝜑𝐾 ∈ ω)
226 nn0suc 7584 . . 3 (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
227225, 226syl 17 . 2 (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
22813, 221, 227mpjaod 856 1 (𝜑 → (𝐻𝐾) ∈ (𝐴o 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wo 843   = wceq 1537  wcel 2114  wrex 3126  Vcvv 3473  wss 3913  c0 4269   class class class wbr 5042  Tr wtr 5148   E cep 5440   We wwe 5489  dom cdm 5531  cima 5534  Ord word 6166  Oncon0 6167  suc csuc 6169   Fn wfn 6326  wf 6327  cfv 6331   Isom wiso 6332  (class class class)co 7133  cmpo 7135  ωcom 7558   supp csupp 7808  seqωcseqom 8061   +o coa 8077   ·o comu 8078  o coe 8079   finSupp cfsupp 8811  OrdIsocoi 8951   CNF ccnf 9102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-supp 7809  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-seqom 8062  df-1o 8080  df-2o 8081  df-oadd 8084  df-omul 8085  df-oexp 8086  df-er 8267  df-map 8386  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-fsupp 8812  df-oi 8952  df-cnf 9103
This theorem is referenced by:  cantnflt2  9114  cnfcomlem  9140
  Copyright terms: Public domain W3C validator