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

Theorem cantnflt 9712
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 8624 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
51, 2, 3, 4syl21anc 838 . . 3 (𝜑 → ∅ ∈ (𝐴o 𝐶))
6 fveq2 6906 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 5307 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
98seqom0g 8496 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10eqtrdi 2793 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2826 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴o 𝐶) ↔ ∅ ∈ (𝐴o 𝐶)))
135, 12syl5ibrcom 247 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴o 𝐶)))
142adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 6394 . . . . . . 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 9570 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6736 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 9569 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 7833 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 230 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 6408 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 587 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 6473 . . . . . . . . . . 11 ((𝐾 ∈ On ∧ Ord dom 𝐺) → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3028, 24, 29sylancl 586 . . . . . . . . . 10 (𝜑 → (𝐾 ⊆ dom 𝐺𝐾 ∈ suc dom 𝐺))
3123, 30mpbird 257 . . . . . . . . 9 (𝜑𝐾 ⊆ dom 𝐺)
3231adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ⊆ dom 𝐺)
33 vex 3484 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 6466 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 773 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35eleqtrrid 2848 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 7253 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1373 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 3984 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7838 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 8202 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . 13 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . 14 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 9706 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 232 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 494 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝐴)
4942, 48fssdm 6755 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
50 onss 7805 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5145, 50syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5249, 51sstrd 3994 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5352adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5423adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5535, 54eqeltrrd 2842 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc 𝑥 ∈ suc dom 𝐺)
56 ordsucelsuc 7842 . . . . . . . . . . 11 (Ord dom 𝐺 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺))
5724, 56ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ dom 𝐺 ↔ suc 𝑥 ∈ suc dom 𝐺)
5855, 57sylibr 234 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ dom 𝐺)
5920ffvelcdmi 7103 . . . . . . . . 9 (𝑥 ∈ dom 𝐺 → (𝐺𝑥) ∈ (𝐹 supp ∅))
6058, 59syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐹 supp ∅))
6153, 60sseldd 3984 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ On)
62 onsuc 7831 . . . . . . 7 ((𝐺𝑥) ∈ On → suc (𝐺𝑥) ∈ On)
6361, 62syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ∈ On)
641adantr 480 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐴 ∈ On)
653adantr 480 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → ∅ ∈ 𝐴)
66 oewordi 8629 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6763, 14, 64, 65, 66syl31anc 1375 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6841, 67mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶))
6935fveq2d 6910 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
70 simprl 771 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
71 simpl 482 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
72 eleq1 2829 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
73 suceq 6450 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7473fveq2d 6910 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
75 fveq2 6906 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
76 suceq 6450 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7775, 76syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
7877oveq2d 7447 . . . . . . . . 9 (𝑥 = ∅ → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘∅)))
7974, 78eleq12d 2835 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
8072, 79imbi12d 344 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))))
81 eleq1 2829 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
82 suceq 6450 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8382fveq2d 6910 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
84 fveq2 6906 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
85 suceq 6450 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8684, 85syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8786oveq2d 7447 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺𝑦)))
8883, 87eleq12d 2835 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
8981, 88imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))))
90 eleq1 2829 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
91 suceq 6450 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9291fveq2d 6910 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
93 fveq2 6906 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
94 suceq 6450 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9593, 94syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9695oveq2d 7447 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘suc 𝑦)))
9792, 96eleq12d 2835 . . . . . . . 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 7103 . . . . . . . . . . . 12 (∅ ∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅))
10149sselda 3983 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
102100, 101sylan2 593 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
10399, 102ffvelcdmd 7105 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1041adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
105 onelon 6409 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
106104, 103, 105syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10752sselda 3983 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
108100, 107sylan2 593 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
109 oecl 8575 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o (𝐺‘∅)) ∈ On)
110104, 108, 109syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o (𝐺‘∅)) ∈ On)
1113adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
112 oen0 8624 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o (𝐺‘∅)))
113104, 108, 111, 112syl21anc 838 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴o (𝐺‘∅)))
114 omord2 8605 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴o (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
115106, 104, 110, 113, 114syl31anc 1375 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
116103, 115mpbid 232 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴))
117 peano1 7910 . . . . . . . . . . . 12 ∅ ∈ ω
118117a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
11944, 1, 45, 19, 43, 8cantnfsuc 9710 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ ω) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
120118, 119sylan2 593 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)))
12110oveq2i 7442 . . . . . . . . . . 11 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅)
122 omcl 8574 . . . . . . . . . . . . 13 (((𝐴o (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
123110, 106, 122syl2anc 584 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
124 oa0 8554 . . . . . . . . . . . 12 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
125123, 124syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
126121, 125eqtrid 2789 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
127120, 126eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
128 oesuc 8565 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
129104, 108, 128syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
130116, 127, 1293eltr4d 2856 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))
131130ex 412 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
132 ordtr 6398 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13324, 132ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
134 trsuc 6471 . . . . . . . . . . 11 ((Tr dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺)
135133, 134mpan 690 . . . . . . . . . 10 (suc 𝑦 ∈ dom 𝐺𝑦 ∈ dom 𝐺)
136135imim1i 63 . . . . . . . . 9 ((𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))) → (suc 𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
1371ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐴 ∈ On)
138 eloni 6394 . . . . . . . . . . . . . . . 16 (𝐴 ∈ On → Ord 𝐴)
139137, 138syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord 𝐴)
14048ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐹:𝐵𝐴)
14149ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ 𝐵)
14220ffvelcdmi 7103 . . . . . . . . . . . . . . . . . 18 (suc 𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
143142ad2antrl 728 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅))
144141, 143sseldd 3984 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ 𝐵)
145140, 144ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴)
146 ordsucss 7838 . . . . . . . . . . . . . . 15 (Ord 𝐴 → ((𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴 → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴))
147139, 145, 146sylc 65 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴)
148 onelon 6409 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘suc 𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
149137, 145, 148syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
150 onsuc 7831 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐺‘suc 𝑦)) ∈ On → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
151149, 150syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On)
15252ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐹 supp ∅) ⊆ On)
153152, 143sseldd 3984 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
154 oecl 8575 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
155137, 153, 154syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
156 omwordi 8609 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴)))
157151, 137, 155, 156syl3anc 1373 . . . . . . . . . . . . . 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 8565 . . . . . . . . . . . . . 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 4021 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴o suc (𝐺‘suc 𝑦)))
162 eloni 6394 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
163153, 162syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
164 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
165164sucid 6466 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
166164sucex 7826 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
167166epeli 5586 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
168165, 167mpbir 231 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
169 ovexd 7466 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17044, 1, 45, 19, 43cantnfcl 9707 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
171170simpld 494 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17219oiiso 9577 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
173169, 171, 172syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
174173ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
175135ad2antrl 728 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → 𝑦 ∈ dom 𝐺)
176 simprl 771 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ dom 𝐺)
177 isorel 7346 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
178174, 175, 176, 177syl12anc 837 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝑦 E suc 𝑦 ↔ (𝐺𝑦) E (𝐺‘suc 𝑦)))
179168, 178mpbii 233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) E (𝐺‘suc 𝑦))
180 fvex 6919 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
181180epeli 5586 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
182179, 181sylib 218 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐺‘suc 𝑦))
183 ordsucss 7838 . . . . . . . . . . . . . . . . 17 (Ord (𝐺‘suc 𝑦) → ((𝐺𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)))
184163, 182, 183sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦))
18520ffvelcdmi 7103 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
186175, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ (𝐹 supp ∅))
187152, 186sseldd 3984 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺𝑦) ∈ On)
188 onsuc 7831 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑦) ∈ On → suc (𝐺𝑦) ∈ On)
189187, 188syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc (𝐺𝑦) ∈ On)
1903ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ∅ ∈ 𝐴)
191 oewordi 8629 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴o suc (𝐺𝑦)) ⊆ (𝐴o (𝐺‘suc 𝑦))))
192189, 153, 137, 190, 191syl31anc 1375 . . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))
195193, 194sseldd 3984 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)))
196 peano2 7912 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
197196ad2antlr 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
1988cantnfvalf 9705 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
199198ffvelcdmi 7103 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
200197, 199syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
201 omcl 8574 . . . . . . . . . . . . . . . 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 8585 . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . 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 9710 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ ω) → (𝐻‘suc suc 𝑦) = (((𝐴o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))) +o (𝐻‘suc 𝑦)))
207196, 206sylan2 593 . . . . . . . . . . . . . 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 8564 . . . . . . . . . . . . . 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 2856 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))))
212161, 211sseldd 3984 . . . . . . . . . . 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 7920 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))))
21870, 71, 58, 217syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))
21969, 218eqeltrd 2841 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o suc (𝐺𝑥)))
22068, 219sseldd 3984 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o 𝐶))
221220rexlimdvaa 3156 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴o 𝐶)))
222 peano2 7912 . . . . 5 (dom 𝐺 ∈ ω → suc dom 𝐺 ∈ ω)
223170, 222simpl2im 503 . . . 4 (𝜑 → suc dom 𝐺 ∈ ω)
224 elnn 7898 . . . 4 ((𝐾 ∈ suc dom 𝐺 ∧ suc dom 𝐺 ∈ ω) → 𝐾 ∈ ω)
22523, 223, 224syl2anc 584 . . 3 (𝜑𝐾 ∈ ω)
226 nn0suc 7916 . . 3 (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
227225, 226syl 17 . 2 (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
22813, 221, 227mpjaod 861 1 (𝜑 → (𝐻𝐾) ∈ (𝐴o 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  wrex 3070  Vcvv 3480  wss 3951  c0 4333   class class class wbr 5143  Tr wtr 5259   E cep 5583   We wwe 5636  dom cdm 5685  cima 5688  Ord word 6383  Oncon0 6384  suc csuc 6386   Fn wfn 6556  wf 6557  cfv 6561   Isom wiso 6562  (class class class)co 7431  cmpo 7433  ωcom 7887   supp csupp 8185  seqωcseqom 8487   +o coa 8503   ·o comu 8504  o coe 8505   finSupp cfsupp 9401  OrdIsocoi 9549   CNF ccnf 9701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-seqom 8488  df-1o 8506  df-2o 8507  df-oadd 8510  df-omul 8511  df-oexp 8512  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-oi 9550  df-cnf 9702
This theorem is referenced by:  cantnflt2  9713  cnfcomlem  9739
  Copyright terms: Public domain W3C validator