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

Theorem cantnflt 9710
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 8623 . . . 4 (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐶))
51, 2, 3, 4syl21anc 838 . . 3 (𝜑 → ∅ ∈ (𝐴o 𝐶))
6 fveq2 6907 . . . . 5 (𝐾 = ∅ → (𝐻𝐾) = (𝐻‘∅))
7 0ex 5313 . . . . . 6 ∅ ∈ V
8 cantnfval.h . . . . . . 7 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
98seqom0g 8495 . . . . . 6 (∅ ∈ V → (𝐻‘∅) = ∅)
107, 9ax-mp 5 . . . . 5 (𝐻‘∅) = ∅
116, 10eqtrdi 2791 . . . 4 (𝐾 = ∅ → (𝐻𝐾) = ∅)
1211eleq1d 2824 . . 3 (𝐾 = ∅ → ((𝐻𝐾) ∈ (𝐴o 𝐶) ↔ ∅ ∈ (𝐴o 𝐶)))
135, 12syl5ibrcom 247 . 2 (𝜑 → (𝐾 = ∅ → (𝐻𝐾) ∈ (𝐴o 𝐶)))
142adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐶 ∈ On)
15 eloni 6396 . . . . . . 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 9568 . . . . . . . . 9 𝐺:dom 𝐺⟶(𝐹 supp ∅)
21 ffn 6737 . . . . . . . . 9 (𝐺:dom 𝐺⟶(𝐹 supp ∅) → 𝐺 Fn dom 𝐺)
2220, 21mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐺 Fn dom 𝐺)
23 cantnflt.k . . . . . . . . . 10 (𝜑𝐾 ∈ suc dom 𝐺)
2419oicl 9567 . . . . . . . . . . . . 13 Ord dom 𝐺
25 ordsuc 7833 . . . . . . . . . . . . 13 (Ord dom 𝐺 ↔ Ord suc dom 𝐺)
2624, 25mpbi 230 . . . . . . . . . . . 12 Ord suc dom 𝐺
27 ordelon 6410 . . . . . . . . . . . 12 ((Ord suc dom 𝐺𝐾 ∈ suc dom 𝐺) → 𝐾 ∈ On)
2826, 23, 27sylancr 587 . . . . . . . . . . 11 (𝜑𝐾 ∈ On)
29 ordsssuc 6475 . . . . . . . . . . 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 3482 . . . . . . . . . 10 𝑥 ∈ V
3433sucid 6468 . . . . . . . . 9 𝑥 ∈ suc 𝑥
35 simprr 773 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 = suc 𝑥)
3634, 35eleqtrrid 2846 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥𝐾)
37 fnfvima 7253 . . . . . . . 8 ((𝐺 Fn dom 𝐺𝐾 ⊆ dom 𝐺𝑥𝐾) → (𝐺𝑥) ∈ (𝐺𝐾))
3822, 32, 36, 37syl3anc 1370 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ (𝐺𝐾))
3918, 38sseldd 3996 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐺𝑥) ∈ 𝐶)
40 ordsucss 7838 . . . . . 6 (Ord 𝐶 → ((𝐺𝑥) ∈ 𝐶 → suc (𝐺𝑥) ⊆ 𝐶))
4116, 39, 40sylc 65 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → suc (𝐺𝑥) ⊆ 𝐶)
42 suppssdm 8201 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
43 cantnfcl.f . . . . . . . . . . . . 13 (𝜑𝐹𝑆)
44 cantnfs.s . . . . . . . . . . . . . 14 𝑆 = dom (𝐴 CNF 𝐵)
45 cantnfs.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ On)
4644, 1, 45cantnfs 9704 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
4743, 46mpbid 232 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
4847simpld 494 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝐴)
4942, 48fssdm 6756 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
50 onss 7804 . . . . . . . . . . 11 (𝐵 ∈ On → 𝐵 ⊆ On)
5145, 50syl 17 . . . . . . . . . 10 (𝜑𝐵 ⊆ On)
5249, 51sstrd 4006 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ⊆ On)
5352adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐹 supp ∅) ⊆ On)
5423adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝐾 ∈ suc dom 𝐺)
5535, 54eqeltrrd 2840 . . . . . . . . . 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 3996 . . . . . . 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 8628 . . . . . 6 (((suc (𝐺𝑥) ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6763, 14, 64, 65, 66syl31anc 1372 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (suc (𝐺𝑥) ⊆ 𝐶 → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶)))
6841, 67mpd 15 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐴o suc (𝐺𝑥)) ⊆ (𝐴o 𝐶))
6935fveq2d 6911 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) = (𝐻‘suc 𝑥))
70 simprl 771 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝑥 ∈ ω)
71 simpl 482 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → 𝜑)
72 eleq1 2827 . . . . . . . 8 (𝑥 = ∅ → (𝑥 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺))
73 suceq 6452 . . . . . . . . . 10 (𝑥 = ∅ → suc 𝑥 = suc ∅)
7473fveq2d 6911 . . . . . . . . 9 (𝑥 = ∅ → (𝐻‘suc 𝑥) = (𝐻‘suc ∅))
75 fveq2 6907 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐺𝑥) = (𝐺‘∅))
76 suceq 6452 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘∅) → suc (𝐺𝑥) = suc (𝐺‘∅))
7775, 76syl 17 . . . . . . . . . 10 (𝑥 = ∅ → suc (𝐺𝑥) = suc (𝐺‘∅))
7877oveq2d 7447 . . . . . . . . 9 (𝑥 = ∅ → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘∅)))
7974, 78eleq12d 2833 . . . . . . . 8 (𝑥 = ∅ → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
8072, 79imbi12d 344 . . . . . . 7 (𝑥 = ∅ → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))))
81 eleq1 2827 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝐺𝑦 ∈ dom 𝐺))
82 suceq 6452 . . . . . . . . . 10 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
8382fveq2d 6911 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc 𝑦))
84 fveq2 6907 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
85 suceq 6452 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺𝑦) → suc (𝐺𝑥) = suc (𝐺𝑦))
8684, 85syl 17 . . . . . . . . . 10 (𝑥 = 𝑦 → suc (𝐺𝑥) = suc (𝐺𝑦))
8786oveq2d 7447 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺𝑦)))
8883, 87eleq12d 2833 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)) ↔ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦))))
8981, 88imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥))) ↔ (𝑦 ∈ dom 𝐺 → (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))))
90 eleq1 2827 . . . . . . . 8 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺))
91 suceq 6452 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
9291fveq2d 6911 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻‘suc 𝑥) = (𝐻‘suc suc 𝑦))
93 fveq2 6907 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐺𝑥) = (𝐺‘suc 𝑦))
94 suceq 6452 . . . . . . . . . . 11 ((𝐺𝑥) = (𝐺‘suc 𝑦) → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9593, 94syl 17 . . . . . . . . . 10 (𝑥 = suc 𝑦 → suc (𝐺𝑥) = suc (𝐺‘suc 𝑦))
9695oveq2d 7447 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐴o suc (𝐺𝑥)) = (𝐴o suc (𝐺‘suc 𝑦)))
9792, 96eleq12d 2833 . . . . . . . 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 3995 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ 𝐵)
102100, 101sylan2 593 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ 𝐵)
10399, 102ffvelcdmd 7105 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ 𝐴)
1041adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On)
105 onelon 6411 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ 𝐴) → (𝐹‘(𝐺‘∅)) ∈ On)
106104, 103, 105syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐹‘(𝐺‘∅)) ∈ On)
10752sselda 3995 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺‘∅) ∈ (𝐹 supp ∅)) → (𝐺‘∅) ∈ On)
108100, 107sylan2 593 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On)
109 oecl 8574 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o (𝐺‘∅)) ∈ On)
110104, 108, 109syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o (𝐺‘∅)) ∈ On)
1113adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ 𝐴)
112 oen0 8623 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o (𝐺‘∅)))
113104, 108, 111, 112syl21anc 838 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (𝐴o (𝐺‘∅)))
114 omord2 8604 . . . . . . . . . . 11 ((((𝐹‘(𝐺‘∅)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘∅)) ∈ On) ∧ ∅ ∈ (𝐴o (𝐺‘∅))) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
115106, 104, 110, 113, 114syl31anc 1372 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐹‘(𝐺‘∅)) ∈ 𝐴 ↔ ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴)))
116103, 115mpbid 232 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ ((𝐴o (𝐺‘∅)) ·o 𝐴))
117 peano1 7911 . . . . . . . . . . . 12 ∅ ∈ ω
118117a1i 11 . . . . . . . . . . 11 (∅ ∈ dom 𝐺 → ∅ ∈ ω)
11944, 1, 45, 19, 43, 8cantnfsuc 9708 . . . . . . . . . . 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 8573 . . . . . . . . . . . . 13 (((𝐴o (𝐺‘∅)) ∈ On ∧ (𝐹‘(𝐺‘∅)) ∈ On) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
123110, 106, 122syl2anc 584 . . . . . . . . . . . 12 ((𝜑 ∧ ∅ ∈ dom 𝐺) → ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On)
124 oa0 8553 . . . . . . . . . . . 12 (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) ∈ On → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
125123, 124syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
126121, 125eqtrid 2787 . . . . . . . . . 10 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))) +o (𝐻‘∅)) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
127120, 126eqtrd 2775 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) = ((𝐴o (𝐺‘∅)) ·o (𝐹‘(𝐺‘∅))))
128 oesuc 8564 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐺‘∅) ∈ On) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
129104, 108, 128syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐴o suc (𝐺‘∅)) = ((𝐴o (𝐺‘∅)) ·o 𝐴))
130116, 127, 1293eltr4d 2854 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅)))
131130ex 412 . . . . . . 7 (𝜑 → (∅ ∈ dom 𝐺 → (𝐻‘suc ∅) ∈ (𝐴o suc (𝐺‘∅))))
132 ordtr 6400 . . . . . . . . . . . 12 (Ord dom 𝐺 → Tr dom 𝐺)
13324, 132ax-mp 5 . . . . . . . . . . 11 Tr dom 𝐺
134 trsuc 6473 . . . . . . . . . . 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 6396 . . . . . . . . . . . . . . . 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 3996 . . . . . . . . . . . . . . . 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 6411 . . . . . . . . . . . . . . . . 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 3996 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐺‘suc 𝑦) ∈ On)
154 oecl 8574 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ On ∧ (𝐺‘suc 𝑦) ∈ On) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
155137, 153, 154syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐴o (𝐺‘suc 𝑦)) ∈ On)
156 omwordi 8608 . . . . . . . . . . . . . . 15 ((suc (𝐹‘(𝐺‘suc 𝑦)) ∈ On ∧ 𝐴 ∈ On ∧ (𝐴o (𝐺‘suc 𝑦)) ∈ On) → (suc (𝐹‘(𝐺‘suc 𝑦)) ⊆ 𝐴 → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ ((𝐴o (𝐺‘suc 𝑦)) ·o 𝐴)))
157151, 137, 155, 156syl3anc 1370 . . . . . . . . . . . . . 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 8564 . . . . . . . . . . . . . 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 4037 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))) ⊆ (𝐴o suc (𝐺‘suc 𝑦)))
162 eloni 6396 . . . . . . . . . . . . . . . . . 18 ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦))
163153, 162syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → Ord (𝐺‘suc 𝑦))
164 vex 3482 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
165164sucid 6468 . . . . . . . . . . . . . . . . . . . 20 𝑦 ∈ suc 𝑦
166164sucex 7826 . . . . . . . . . . . . . . . . . . . . 21 suc 𝑦 ∈ V
167166epeli 5591 . . . . . . . . . . . . . . . . . . . 20 (𝑦 E suc 𝑦𝑦 ∈ suc 𝑦)
168165, 167mpbir 231 . . . . . . . . . . . . . . . . . . 19 𝑦 E suc 𝑦
169 ovexd 7466 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 supp ∅) ∈ V)
17044, 1, 45, 19, 43cantnfcl 9705 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
171170simpld 494 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → E We (𝐹 supp ∅))
17219oiiso 9575 . . . . . . . . . . . . . . . . . . . . . 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 6920 . . . . . . . . . . . . . . . . . . 19 (𝐺‘suc 𝑦) ∈ V
181180epeli 5591 . . . . . . . . . . . . . . . . . 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 3996 . . . . . . . . . . . . . . . . . 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 8628 . . . . . . . . . . . . . . . . 17 (((suc (𝐺𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (suc (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴o suc (𝐺𝑦)) ⊆ (𝐴o (𝐺‘suc 𝑦))))
192189, 153, 137, 190, 191syl31anc 1372 . . . . . . . . . . . . . . . 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 3996 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ (𝐴o (𝐺‘suc 𝑦)))
196 peano2 7913 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
197196ad2antlr 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → suc 𝑦 ∈ ω)
1988cantnfvalf 9703 . . . . . . . . . . . . . . . . 17 𝐻:ω⟶On
199198ffvelcdmi 7103 . . . . . . . . . . . . . . . 16 (suc 𝑦 ∈ ω → (𝐻‘suc 𝑦) ∈ On)
200197, 199syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc 𝑦) ∈ On)
201 omcl 8573 . . . . . . . . . . . . . . . 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 8584 . . . . . . . . . . . . . . 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 1370 . . . . . . . . . . . . . 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 9708 . . . . . . . . . . . . . . 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 8563 . . . . . . . . . . . . . 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 2854 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝐻‘suc 𝑦) ∈ (𝐴o suc (𝐺𝑦)))) → (𝐻‘suc suc 𝑦) ∈ ((𝐴o (𝐺‘suc 𝑦)) ·o suc (𝐹‘(𝐺‘suc 𝑦))))
212161, 211sseldd 3996 . . . . . . . . . . 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 7921 . . . . . 6 (𝑥 ∈ ω → (𝜑 → (𝑥 ∈ dom 𝐺 → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))))
21870, 71, 58, 217syl3c 66 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻‘suc 𝑥) ∈ (𝐴o suc (𝐺𝑥)))
21969, 218eqeltrd 2839 . . . 4 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o suc (𝐺𝑥)))
22068, 219sseldd 3996 . . 3 ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝐾 = suc 𝑥)) → (𝐻𝐾) ∈ (𝐴o 𝐶))
221220rexlimdvaa 3154 . 2 (𝜑 → (∃𝑥 ∈ ω 𝐾 = suc 𝑥 → (𝐻𝐾) ∈ (𝐴o 𝐶)))
222 peano2 7913 . . . . 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 7917 . . 3 (𝐾 ∈ ω → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
227225, 226syl 17 . 2 (𝜑 → (𝐾 = ∅ ∨ ∃𝑥 ∈ ω 𝐾 = suc 𝑥))
22813, 221, 227mpjaod 860 1 (𝜑 → (𝐻𝐾) ∈ (𝐴o 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wcel 2106  wrex 3068  Vcvv 3478  wss 3963  c0 4339   class class class wbr 5148  Tr wtr 5265   E cep 5588   We wwe 5640  dom cdm 5689  cima 5692  Ord word 6385  Oncon0 6386  suc csuc 6388   Fn wfn 6558  wf 6559  cfv 6563   Isom wiso 6564  (class class class)co 7431  cmpo 7433  ωcom 7887   supp csupp 8184  seqωcseqom 8486   +o coa 8502   ·o comu 8503  o coe 8504   finSupp cfsupp 9399  OrdIsocoi 9547   CNF ccnf 9699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-seqom 8487  df-1o 8505  df-2o 8506  df-oadd 8509  df-omul 8510  df-oexp 8511  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-oi 9548  df-cnf 9700
This theorem is referenced by:  cantnflt2  9711  cnfcomlem  9737
  Copyright terms: Public domain W3C validator