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

Theorem cantnflt 9123
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 8201 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
51, 2, 3, 4syl21anc 833 . . 3 (𝜑 → ∅ ∈ (𝐴o 𝐶))
6 fveq2 6663 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 5202 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
98seqom0g 8081 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10syl6eq 2869 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2894 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴o 𝐶) ↔ ∅ ∈ (𝐴o 𝐶)))
135, 12syl5ibrcom 248 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴o 𝐶)))
142adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 6194 . . . . . . 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 8982 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6507 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 8981 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 7518 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 231 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 6208 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 587 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 6270 . . . . . . . . . . 11 ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3028, 24, 29sylancl 586 . . . . . . . . . 10 (𝜑 → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3123, 30mpbird 258 . . . . . . . . 9 (𝜑𝐾 ⊆ dom 𝐺)
3231adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33 vex 3495 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 6263 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 769 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35eleqtrrid 2917 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 6986 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1363 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 3965 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7522 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 7832 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . 13 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . 14 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 9117 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 233 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 495 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝐴)
4942, 48fssdm 6523 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
50 onss 7494 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5145, 50syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5249, 51sstrd 3974 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5352adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5423adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5535, 54eqeltrrd 2911 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
56 ordsucelsuc 7526 . . . . . . . . . . 11 (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
5724, 56ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
5855, 57sylibr 235 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
5920ffvelrni 6842 . . . . . . . . 9 (𝑥 ∈ dom 𝐺 → (𝐺𝑥) ∈ (𝐹 supp ∅))
6058, 59syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐹 supp ∅))
6153, 60sseldd 3965 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ On)
62 suceloni 7517 . . . . . . 7 ((𝐺𝑥) ∈ On → suc (𝐺𝑥) ∈ On)
6361, 62syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ∈ On)
641adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
653adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
66 oewordi 8206 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6763, 14, 64, 65, 66syl31anc 1365 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6841, 67mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶))
6935fveq2d 6667 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
70 simprl 767 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
71 simpl 483 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
72 eleq1 2897 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
73 suceq 6249 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7473fveq2d 6667 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
75 fveq2 6663 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
76 suceq 6249 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7775, 76syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
7877oveq2d 7161 . . . . . . . . 9 (𝑥 = ∅ → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘∅)))
7974, 78eleq12d 2904 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
8072, 79imbi12d 346 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))))
81 eleq1 2897 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
82 suceq 6249 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8382fveq2d 6667 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
84 fveq2 6663 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
85 suceq 6249 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8684, 85syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8786oveq2d 7161 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺𝑦)))
8883, 87eleq12d 2904 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
8981, 88imbi12d 346 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))))
90 eleq1 2897 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
91 suceq 6249 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9291fveq2d 6667 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
93 fveq2 6663 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
94 suceq 6249 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9593, 94syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9695oveq2d 7161 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘suc 𝑦)))
9792, 96eleq12d 2904 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦))))
9890, 97imbi12d 346 . . . . . . 7 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))))
9948adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐹:𝐵𝐴)
10020ffvelrni 6842 . . . . . . . . . . . 12 (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
10149sselda 3964 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
102100, 101sylan2 592 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
10399, 102ffvelrnd 6844 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1041adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
105 onelon 6209 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
106104, 103, 105syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10752sselda 3964 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
108100, 107sylan2 592 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
109 oecl 8151 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o (𝐺‘∅)) ∈ On)
110104, 108, 109syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o (𝐺‘∅)) ∈ On)
1113adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
112 oen0 8201 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o (𝐺‘∅)))
113104, 108, 111, 112syl21anc 833 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴o (𝐺‘∅)))
114 omord2 8182 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴o (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
115106, 104, 110, 113, 114syl31anc 1365 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
116103, 115mpbid 233 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴))
117 peano1 7590 . . . . . . . . . . . 12 ∅ ∈ ω
118117a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
11944, 1, 45, 19, 43, 8cantnfsuc 9121 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
120118, 119sylan2 592 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
12110oveq2i 7156 . . . . . . . . . . 11 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅)
122 omcl 8150 . . . . . . . . . . . . 13 (((𝐴o (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
123110, 106, 122syl2anc 584 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
124 oa0 8130 . . . . . . . . . . . 12 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
125123, 124syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
126121, 125syl5eq 2865 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
127120, 126eqtrd 2853 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
128 oesuc 8141 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
129104, 108, 128syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
130116, 127, 1293eltr4d 2925 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))
131130ex 413 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
132 ordtr 6198 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13324, 132ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
134 trsuc 6268 . . . . . . . . . . 11 ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
135133, 134mpan 686 . . . . . . . . . 10 (suc 𝑦 ∈ dom 𝐺𝑦 ∈ dom 𝐺)
136135imim1i 63 . . . . . . . . 9 ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
1371ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐴 ∈ On)
138 eloni 6194 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → Ord 𝐴)
139137, 138syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord 𝐴)
14048ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐹:𝐵𝐴)
14149ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
14220ffvelrni 6842 . . . . . . . . . . . . . . . . . 18 (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
143142ad2antrl 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
144141, 143sseldd 3965 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
145140, 144ffvelrnd 6844 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
146 ordsucss 7522 . . . . . . . . . . . . . . 15 (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
147139, 145, 146sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
148 onelon 6209 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
149137, 145, 148syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
150 suceloni 7517 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151149, 150syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
15252ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ On)
153152, 143sseldd 3965 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
154 oecl 8151 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
155137, 153, 154syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
156 omwordi 8186 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴)))
157151, 137, 155, 156syl3anc 1363 . . . . . . . . . . . . . 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 8141 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o suc (𝐺‘suc 𝑦)) = ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴))
160137, 153, 159syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o suc (𝐺‘suc 𝑦)) = ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴))
161158, 160sseqtrrd 4005 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴o suc (𝐺‘suc 𝑦)))
162 eloni 6194 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
163153, 162syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
164 vex 3495 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
165164sucid 6263 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
166164sucex 7515 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
167166epeli 5461 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
168165, 167mpbir 232 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
169 ovexd 7180 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17044, 1, 45, 19, 43cantnfcl 9118 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
171170simpld 495 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17219oiiso 8989 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
173169, 171, 172syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
174173ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175135ad2antrl 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝑦 ∈ dom 𝐺)
176 simprl 767 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ dom 𝐺)
177 isorel 7068 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
178174, 175, 176, 177syl12anc 832 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
179168, 178mpbii 234 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) E (𝐺‘suc 𝑦))
180 fvex 6676 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
181180epeli 5461 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
182179, 181sylib 219 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
183 ordsucss 7522 . . . . . . . . . . . . . . . . 17 (Ord (𝐺‘suc 𝑦) → ((𝐺𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)))
184163, 182, 183sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦))
18520ffvelrni 6842 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
186175, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐹 supp ∅))
187152, 186sseldd 3965 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ On)
188 suceloni 7517 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) ∈ On → suc (𝐺𝑦) ∈ On)
189187, 188syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ∈ On)
1903ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ∅ ∈ 𝐴)
191 oewordi 8206 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴o suc (𝐺𝑦)) ⊆ (𝐴o (𝐺‘suc 𝑦))))
192189, 153, 137, 190, 191syl31anc 1365 . . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))
195193, 194sseldd 3965 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)))
196 peano2 7591 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
197196ad2antlr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
1988cantnfvalf 9116 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
199198ffvelrni 6842 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
200197, 199syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
201 omcl 8150 . . . . . . . . . . . . . . . 16 (((𝐴o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
202155, 149, 201syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) ∈ On)
203 oaord 8162 . . . . . . . . . . . . . . 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 1363 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)) ↔ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)) ∈ (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦)))))
205195, 204mpbid 233 . . . . . . . . . . . . 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 9121 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
207196, 206sylan2 592 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
208207adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
209 omsuc 8140 . . . . . . . . . . . . . 14 (((𝐴o (𝐺‘suc 𝑦)) ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ On) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦))))
210155, 149, 209syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐴o (𝐺‘suc 𝑦))))
211205, 208, 2103eltr4d 2925 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))))
212161, 211sseldd 3965 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦)))
213212exp32 421 . . . . . . . . . 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 414 . . . . . . 7 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc suc 𝑦) ∈ (𝐴o suc (𝐺‘suc 𝑦))))))
21780, 89, 98, 131, 216finds2 7599 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))))
21870, 71, 58, 217syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))
21969, 218eqeltrd 2910 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o suc (𝐺𝑥)))
22068, 219sseldd 3965 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o 𝐶))
221220rexlimdvaa 3282 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴o 𝐶)))
222 peano2 7591 . . . . 5 (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
223170, 222simpl2im 504 . . . 4 (𝜑 → suc dom 𝐺 ∈ ω)
224 elnn 7579 . . . 4 ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
22523, 223, 224syl2anc 584 . . 3 (𝜑𝐾 ∈ ω)
226 nn0suc 7595 . . 3 (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
227225, 226syl 17 . 2 (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
22813, 221, 227mpjaod 854 1 (𝜑 → (𝐻𝐾) ∈ (𝐴o 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  wrex 3136  Vcvv 3492  wss 3933  c0 4288   class class class wbr 5057  Tr wtr 5163   E cep 5457   We wwe 5506  dom cdm 5548  cima 5551  Ord word 6183  Oncon0 6184  suc csuc 6186   Fn wfn 6343  wf 6344  cfv 6348   Isom wiso 6349  (class class class)co 7145  cmpo 7147  ωcom 7569   supp csupp 7819  seqωcseqom 8072   +o coa 8088   ·o comu 8089  o coe 8090   finSupp cfsupp 8821  OrdIsocoi 8961   CNF ccnf 9112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-seqom 8073  df-1o 8091  df-2o 8092  df-oadd 8095  df-omul 8096  df-oexp 8097  df-er 8278  df-map 8397  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-oi 8962  df-cnf 9113
This theorem is referenced by:  cantnflt2  9124  cnfcomlem  9150
  Copyright terms: Public domain W3C validator