Step | Hyp | Ref
| Expression |
1 | | omelon 8543 |
. . . . . . 7
⊢ ω
∈ On |
2 | | cnfcom.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ On) |
3 | | suppssdm 7308 |
. . . . . . . . . 10
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
4 | | cnfcom.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) |
5 | | cnfcom.s |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = dom (ω CNF 𝐴) |
6 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ω ∈
On) |
7 | 5, 6, 2 | cantnff1o 8593 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴)) |
8 | | f1ocnv 6149 |
. . . . . . . . . . . . . . . 16
⊢ ((ω
CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆) |
9 | | f1of 6137 |
. . . . . . . . . . . . . . . 16
⊢ (◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
11 | | cnfcom.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜
𝐴)) |
12 | 10, 11 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆) |
13 | 4, 12 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
14 | 5, 6, 2 | cantnfs 8563 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))) |
15 | 13, 14 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)) |
16 | 15 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ω) |
17 | | fdm 6051 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ω → dom 𝐹 = 𝐴) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝐴) |
19 | 3, 18 | syl5sseq 3653 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴) |
20 | | cnfcom.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ dom 𝐺) |
21 | | cnfcom.g |
. . . . . . . . . . . 12
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
22 | 21 | oif 8435 |
. . . . . . . . . . 11
⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅) |
23 | 22 | ffvelrni 6358 |
. . . . . . . . . 10
⊢ (𝐼 ∈ dom 𝐺 → (𝐺‘𝐼) ∈ (𝐹 supp ∅)) |
24 | 20, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝐼) ∈ (𝐹 supp ∅)) |
25 | 19, 24 | sseldd 3604 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐼) ∈ 𝐴) |
26 | | onelon 5748 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝐼) ∈ 𝐴) → (𝐺‘𝐼) ∈ On) |
27 | 2, 25, 26 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐼) ∈ On) |
28 | | oecl 7617 |
. . . . . . 7
⊢ ((ω
∈ On ∧ (𝐺‘𝐼) ∈ On) → (ω
↑𝑜 (𝐺‘𝐼)) ∈ On) |
29 | 1, 27, 28 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → (ω
↑𝑜 (𝐺‘𝐼)) ∈ On) |
30 | 16, 25 | ffvelrnd 6360 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ ω) |
31 | | nnon 7071 |
. . . . . . 7
⊢ ((𝐹‘(𝐺‘𝐼)) ∈ ω → (𝐹‘(𝐺‘𝐼)) ∈ On) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ∈ On) |
33 | | omcl 7616 |
. . . . . 6
⊢
(((ω ↑𝑜 (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) → ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On) |
34 | 29, 32, 33 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On) |
35 | 5, 6, 2, 21, 13 | cantnfcl 8564 |
. . . . . . . 8
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) |
36 | 35 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → dom 𝐺 ∈ ω) |
37 | | elnn 7075 |
. . . . . . 7
⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω) |
38 | 20, 36, 37 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ω) |
39 | | cnfcom.h |
. . . . . . . 8
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (𝑀
+𝑜 𝑧)),
∅) |
40 | 39 | cantnfvalf 8562 |
. . . . . . 7
⊢ 𝐻:ω⟶On |
41 | 40 | ffvelrni 6358 |
. . . . . 6
⊢ (𝐼 ∈ ω → (𝐻‘𝐼) ∈ On) |
42 | 38, 41 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝐼) ∈ On) |
43 | | eqid 2622 |
. . . . . 6
⊢ ((𝑦 ∈ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) = ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) |
44 | 43 | oacomf1o 7645 |
. . . . 5
⊢
((((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On ∧ (𝐻‘𝐼) ∈ On) → ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))) |
45 | 34, 42, 44 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))) |
46 | | cnfcom.t |
. . . . . . . 8
⊢ 𝑇 =
seq𝜔((𝑘
∈ V, 𝑓 ∈ V
↦ 𝐾),
∅) |
47 | 46 | seqomsuc 7552 |
. . . . . . 7
⊢ (𝐼 ∈ ω → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼))) |
48 | 38, 47 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑇‘suc 𝐼) = (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼))) |
49 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑢𝐾 |
50 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑣𝐾 |
51 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))) |
52 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑓((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))) |
53 | | cnfcom.k |
. . . . . . . . . 10
⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) |
54 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (dom 𝑓 +𝑜 𝑥) = (dom 𝑓 +𝑜 𝑦)) |
55 | 54 | cbvmptv 4750 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) = (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑦)) |
56 | | cnfcom.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = ((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) |
57 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑘 = 𝑢) |
58 | 57 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐺‘𝑘) = (𝐺‘𝑢)) |
59 | 58 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (ω ↑𝑜
(𝐺‘𝑘)) = (ω ↑𝑜
(𝐺‘𝑢))) |
60 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑢))) |
61 | 59, 60 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((ω ↑𝑜
(𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) = ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢)))) |
62 | 56, 61 | syl5eq 2668 |
. . . . . . . . . . . . 13
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑀 = ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢)))) |
63 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝑓 = 𝑣) |
64 | 63 | dmeqd 5326 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → dom 𝑓 = dom 𝑣) |
65 | 64 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (dom 𝑓 +𝑜 𝑦) = (dom 𝑣 +𝑜 𝑦)) |
66 | 62, 65 | mpteq12dv 4733 |
. . . . . . . . . . . 12
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑦)) = (𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦))) |
67 | 55, 66 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) = (𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦))) |
68 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝑀 +𝑜 𝑥) = (𝑀 +𝑜 𝑦)) |
69 | 68 | cbvmptv 4750 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)) = (𝑦 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑦)) |
70 | 62 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑀 +𝑜 𝑦) = (((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)) |
71 | 64, 70 | mpteq12dv 4733 |
. . . . . . . . . . . . 13
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑦 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑦)) = (𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))) |
72 | 69, 71 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → (𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)) = (𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))) |
73 | 72 | cnveqd 5298 |
. . . . . . . . . . 11
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥)) = ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))) |
74 | 67, 73 | uneq12d 3768 |
. . . . . . . . . 10
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) = ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))) |
75 | 53, 74 | syl5eq 2668 |
. . . . . . . . 9
⊢ ((𝑘 = 𝑢 ∧ 𝑓 = 𝑣) → 𝐾 = ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))) |
76 | 49, 50, 51, 52, 75 | cbvmpt2 6734 |
. . . . . . . 8
⊢ (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)))) |
77 | 76 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾) = (𝑢 ∈ V, 𝑣 ∈ V ↦ ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))))) |
78 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → 𝑢 = 𝐼) |
79 | 78 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐺‘𝑢) = (𝐺‘𝐼)) |
80 | 79 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (ω
↑𝑜 (𝐺‘𝑢)) = (ω ↑𝑜
(𝐺‘𝐼))) |
81 | 79 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝐹‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝐼))) |
82 | 80, 81 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) = ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) |
83 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → 𝑣 = (𝑇‘𝐼)) |
84 | 83 | dmeqd 5326 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼)) → dom 𝑣 = dom (𝑇‘𝐼)) |
85 | | cnfcom.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂) |
86 | | f1odm 6141 |
. . . . . . . . . . . 12
⊢ ((𝑇‘𝐼):(𝐻‘𝐼)–1-1-onto→𝑂 → dom (𝑇‘𝐼) = (𝐻‘𝐼)) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑇‘𝐼) = (𝐻‘𝐼)) |
88 | 84, 87 | sylan9eqr 2678 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → dom 𝑣 = (𝐻‘𝐼)) |
89 | 88 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (dom 𝑣 +𝑜 𝑦) = ((𝐻‘𝐼) +𝑜 𝑦)) |
90 | 82, 89 | mpteq12dv 4733 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) = (𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦))) |
91 | 82 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦) = (((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)) |
92 | 88, 91 | mpteq12dv 4733 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → (𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)) = (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) |
93 | 92 | cnveqd 5298 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦)) = ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) |
94 | 90, 93 | uneq12d 3768 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 = 𝐼 ∧ 𝑣 = (𝑇‘𝐼))) → ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) ↦ (dom 𝑣 +𝑜 𝑦)) ∪ ◡(𝑦 ∈ dom 𝑣 ↦ (((ω
↑𝑜 (𝐺‘𝑢)) ·𝑜 (𝐹‘(𝐺‘𝑢))) +𝑜 𝑦))) = ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)))) |
95 | | elex 3212 |
. . . . . . . 8
⊢ (𝐼 ∈ dom 𝐺 → 𝐼 ∈ V) |
96 | 20, 95 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ V) |
97 | | fvexd 6203 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘𝐼) ∈ V) |
98 | | ovex 6678 |
. . . . . . . . . 10
⊢ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ V |
99 | 98 | mptex 6486 |
. . . . . . . . 9
⊢ (𝑦 ∈ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∈ V |
100 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝐻‘𝐼) ∈ V |
101 | 100 | mptex 6486 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)) ∈ V |
102 | 101 | cnvex 7113 |
. . . . . . . . 9
⊢ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)) ∈ V |
103 | 99, 102 | unex 6956 |
. . . . . . . 8
⊢ ((𝑦 ∈ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) ∈ V |
104 | 103 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) ∈ V) |
105 | 77, 94, 96, 97, 104 | ovmpt2d 6788 |
. . . . . 6
⊢ (𝜑 → (𝐼(𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾)(𝑇‘𝐼)) = ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)))) |
106 | 48, 105 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦)))) |
107 | | f1oeq1 6127 |
. . . . 5
⊢ ((𝑇‘suc 𝐼) = ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))) → ((𝑇‘suc 𝐼):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))) |
108 | 106, 107 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑇‘suc 𝐼):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ ((𝑦 ∈ ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ↦ ((𝐻‘𝐼) +𝑜 𝑦)) ∪ ◡(𝑦 ∈ (𝐻‘𝐼) ↦ (((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 𝑦))):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))) |
109 | 45, 108 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝑇‘suc 𝐼):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))) |
110 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → ω ∈ On) |
111 | | simpl 473 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐴 ∈ On) |
112 | | simpr 477 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) → 𝐹 ∈ 𝑆) |
113 | 56 | oveq1i 6660 |
. . . . . . . . . 10
⊢ (𝑀 +𝑜 𝑧) = (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧) |
114 | 113 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +𝑜 𝑧) = (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)) |
115 | 114 | mpt2eq3ia 6720 |
. . . . . . . 8
⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)) |
116 | | eqid 2622 |
. . . . . . . 8
⊢ ∅ =
∅ |
117 | | seqomeq12 7549 |
. . . . . . . 8
⊢ (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)) ∧ ∅ = ∅) →
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (𝑀
+𝑜 𝑧)),
∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅)) |
118 | 115, 116,
117 | mp2an 708 |
. . . . . . 7
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) |
119 | 39, 118 | eqtri 2644 |
. . . . . 6
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) |
120 | 5, 110, 111, 21, 112, 119 | cantnfsuc 8567 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ 𝐼 ∈ ω) → (𝐻‘suc 𝐼) = (((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))) |
121 | 2, 13, 38, 120 | syl21anc 1325 |
. . . 4
⊢ (𝜑 → (𝐻‘suc 𝐼) = (((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))) |
122 | | f1oeq2 6128 |
. . . 4
⊢ ((𝐻‘suc 𝐼) = (((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼)) → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))) |
123 | 121, 122 | syl 17 |
. . 3
⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) +𝑜 (𝐻‘𝐼))–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))))) |
124 | 109, 123 | mpbird 247 |
. 2
⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))) |
125 | | sssucid 5802 |
. . . . . 6
⊢ dom 𝐺 ⊆ suc dom 𝐺 |
126 | 125, 20 | sseldi 3601 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ suc dom 𝐺) |
127 | | epelg 5030 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ dom 𝐺 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼)) |
128 | 20, 127 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 E 𝐼 ↔ 𝑦 ∈ 𝐼)) |
129 | 128 | biimpar 502 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 E 𝐼) |
130 | | ovexd 6680 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) |
131 | 35 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝜑 → E We (𝐹 supp ∅)) |
132 | 21 | oiiso 8442 |
. . . . . . . . . . . 12
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
133 | 130, 131,
132 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
134 | 133 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
135 | 21 | oicl 8434 |
. . . . . . . . . . . 12
⊢ Ord dom
𝐺 |
136 | | ordelss 5739 |
. . . . . . . . . . . 12
⊢ ((Ord dom
𝐺 ∧ 𝐼 ∈ dom 𝐺) → 𝐼 ⊆ dom 𝐺) |
137 | 135, 20, 136 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ⊆ dom 𝐺) |
138 | 137 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑦 ∈ dom 𝐺) |
139 | 20 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐼 ∈ dom 𝐺) |
140 | | isorel 6576 |
. . . . . . . . . 10
⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ 𝐼 ∈ dom 𝐺)) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼))) |
141 | 134, 138,
139, 140 | syl12anc 1324 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑦 E 𝐼 ↔ (𝐺‘𝑦) E (𝐺‘𝐼))) |
142 | 129, 141 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) E (𝐺‘𝐼)) |
143 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝐺‘𝐼) ∈ V |
144 | 143 | epelc 5031 |
. . . . . . . 8
⊢ ((𝐺‘𝑦) E (𝐺‘𝐼) ↔ (𝐺‘𝑦) ∈ (𝐺‘𝐼)) |
145 | 142, 144 | sylib 208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐺‘𝑦) ∈ (𝐺‘𝐼)) |
146 | 145 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼)) |
147 | | ffun 6048 |
. . . . . . . 8
⊢ (𝐺:dom 𝐺⟶(𝐹 supp ∅) → Fun 𝐺) |
148 | 22, 147 | ax-mp 5 |
. . . . . . 7
⊢ Fun 𝐺 |
149 | | funimass4 6247 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐼 ⊆ dom 𝐺) → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))) |
150 | 148, 137,
149 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → ((𝐺 “ 𝐼) ⊆ (𝐺‘𝐼) ↔ ∀𝑦 ∈ 𝐼 (𝐺‘𝑦) ∈ (𝐺‘𝐼))) |
151 | 146, 150 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼)) |
152 | 1 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ω ∈
On) |
153 | | simpll 790 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐴 ∈ On) |
154 | | simplr 792 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐹 ∈ 𝑆) |
155 | | peano1 7085 |
. . . . . . 7
⊢ ∅
∈ ω |
156 | 155 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → ∅ ∈
ω) |
157 | | simpr1 1067 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → 𝐼 ∈ suc dom 𝐺) |
158 | | simpr2 1068 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺‘𝐼) ∈ On) |
159 | | simpr3 1069 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼)) |
160 | 5, 152, 153, 21, 154, 119, 156, 157, 158, 159 | cantnflt 8569 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐹 ∈ 𝑆) ∧ (𝐼 ∈ suc dom 𝐺 ∧ (𝐺‘𝐼) ∈ On ∧ (𝐺 “ 𝐼) ⊆ (𝐺‘𝐼))) → (𝐻‘𝐼) ∈ (ω ↑𝑜
(𝐺‘𝐼))) |
161 | 2, 13, 126, 27, 151, 160 | syl23anc 1333 |
. . . 4
⊢ (𝜑 → (𝐻‘𝐼) ∈ (ω ↑𝑜
(𝐺‘𝐼))) |
162 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ω → 𝐹 Fn 𝐴) |
163 | 16, 162 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn 𝐴) |
164 | | 0ex 4790 |
. . . . . . . . . 10
⊢ ∅
∈ V |
165 | 164 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ∅ ∈
V) |
166 | | elsuppfn 7303 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V) →
((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅))) |
167 | 163, 2, 165, 166 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) ↔ ((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅))) |
168 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐺‘𝐼) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝐼)) ≠ ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅) |
169 | 167, 168 | syl6bi 243 |
. . . . . . 7
⊢ (𝜑 → ((𝐺‘𝐼) ∈ (𝐹 supp ∅) → (𝐹‘(𝐺‘𝐼)) ≠ ∅)) |
170 | 24, 169 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝐺‘𝐼)) ≠ ∅) |
171 | | on0eln0 5780 |
. . . . . . 7
⊢ ((𝐹‘(𝐺‘𝐼)) ∈ On → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅)) |
172 | 32, 171 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∅ ∈ (𝐹‘(𝐺‘𝐼)) ↔ (𝐹‘(𝐺‘𝐼)) ≠ ∅)) |
173 | 170, 172 | mpbird 247 |
. . . . 5
⊢ (𝜑 → ∅ ∈ (𝐹‘(𝐺‘𝐼))) |
174 | | omword1 7653 |
. . . . 5
⊢
((((ω ↑𝑜 (𝐺‘𝐼)) ∈ On ∧ (𝐹‘(𝐺‘𝐼)) ∈ On) ∧ ∅ ∈ (𝐹‘(𝐺‘𝐼))) → (ω
↑𝑜 (𝐺‘𝐼)) ⊆ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) |
175 | 29, 32, 173, 174 | syl21anc 1325 |
. . . 4
⊢ (𝜑 → (ω
↑𝑜 (𝐺‘𝐼)) ⊆ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) |
176 | | oaabs2 7725 |
. . . 4
⊢ ((((𝐻‘𝐼) ∈ (ω ↑𝑜
(𝐺‘𝐼)) ∧ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) ∈ On) ∧ (ω
↑𝑜 (𝐺‘𝐼)) ⊆ ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) → ((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) = ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) |
177 | 161, 34, 175, 176 | syl21anc 1325 |
. . 3
⊢ (𝜑 → ((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) = ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) |
178 | | f1oeq3 6129 |
. . 3
⊢ (((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) = ((ω ↑𝑜
(𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))) → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))) |
179 | 177, 178 | syl 17 |
. 2
⊢ (𝜑 → ((𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((𝐻‘𝐼) +𝑜 ((ω
↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼))))) |
180 | 124, 179 | mpbid 222 |
1
⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑𝑜 (𝐺‘𝐼)) ·𝑜 (𝐹‘(𝐺‘𝐼)))) |