Proof of Theorem cnfcom2
Step | Hyp | Ref
| Expression |
1 | | cnfcom.s |
. . . . 5
⊢ 𝑆 = dom (ω CNF 𝐴) |
2 | | cnfcom.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ On) |
3 | | cnfcom.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜
𝐴)) |
4 | | cnfcom.f |
. . . . 5
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) |
5 | | cnfcom.g |
. . . . 5
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
6 | | cnfcom.h |
. . . . 5
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (𝑀
+𝑜 𝑧)),
∅) |
7 | | cnfcom.t |
. . . . 5
⊢ 𝑇 =
seq𝜔((𝑘
∈ V, 𝑓 ∈ V
↦ 𝐾),
∅) |
8 | | cnfcom.m |
. . . . 5
⊢ 𝑀 = ((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) |
9 | | cnfcom.k |
. . . . 5
⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) |
10 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝐹 supp ∅) ∈
V |
11 | 5 | oion 8324 |
. . . . . . . . . 10
⊢ ((𝐹 supp ∅) ∈ V →
dom 𝐺 ∈
On) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢ dom 𝐺 ∈ On |
13 | 12 | elexi 3186 |
. . . . . . . 8
⊢ dom 𝐺 ∈ V |
14 | 13 | uniex 6851 |
. . . . . . 7
⊢ ∪ dom 𝐺 ∈ V |
15 | 14 | sucid 5721 |
. . . . . 6
⊢ ∪ dom 𝐺 ∈ suc ∪ dom
𝐺 |
16 | | cnfcom.w |
. . . . . . 7
⊢ 𝑊 = (𝐺‘∪ dom
𝐺) |
17 | | cnfcom2.1 |
. . . . . . 7
⊢ (𝜑 → ∅ ∈ 𝐵) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 16,
17 | cnfcom2lem 8481 |
. . . . . 6
⊢ (𝜑 → dom 𝐺 = suc ∪ dom
𝐺) |
19 | 15, 18 | syl5eleqr 2695 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 19 | cnfcom 8480 |
. . . 4
⊢ (𝜑 → (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 (𝐺‘∪ dom 𝐺)) ·𝑜 (𝐹‘(𝐺‘∪ dom
𝐺)))) |
21 | 16 | oveq2i 6560 |
. . . . . 6
⊢ (ω
↑𝑜 𝑊) = (ω ↑𝑜
(𝐺‘∪ dom 𝐺)) |
22 | 16 | fveq2i 6106 |
. . . . . 6
⊢ (𝐹‘𝑊) = (𝐹‘(𝐺‘∪ dom
𝐺)) |
23 | 21, 22 | oveq12i 6561 |
. . . . 5
⊢ ((ω
↑𝑜 𝑊) ·𝑜 (𝐹‘𝑊)) = ((ω ↑𝑜
(𝐺‘∪ dom 𝐺)) ·𝑜 (𝐹‘(𝐺‘∪ dom
𝐺))) |
24 | | f1oeq3 6042 |
. . . . 5
⊢
(((ω ↑𝑜 𝑊) ·𝑜 (𝐹‘𝑊)) = ((ω ↑𝑜
(𝐺‘∪ dom 𝐺)) ·𝑜 (𝐹‘(𝐺‘∪ dom
𝐺))) → ((𝑇‘suc ∪ dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)) ↔ (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 (𝐺‘∪ dom 𝐺)) ·𝑜 (𝐹‘(𝐺‘∪ dom
𝐺))))) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢ ((𝑇‘suc ∪ dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)) ↔ (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 (𝐺‘∪ dom 𝐺)) ·𝑜 (𝐹‘(𝐺‘∪ dom
𝐺)))) |
26 | 20, 25 | sylibr 223 |
. . 3
⊢ (𝜑 → (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))) |
27 | 18 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (𝑇‘dom 𝐺) = (𝑇‘suc ∪ dom
𝐺)) |
28 | | f1oeq1 6040 |
. . . 4
⊢ ((𝑇‘dom 𝐺) = (𝑇‘suc ∪ dom
𝐺) → ((𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)) ↔ (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)))) |
29 | 27, 28 | syl 17 |
. . 3
⊢ (𝜑 → ((𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)) ↔ (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)))) |
30 | 26, 29 | mpbird 246 |
. 2
⊢ (𝜑 → (𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))) |
31 | 4 | fveq2i 6106 |
. . . . 5
⊢ ((ω
CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) |
32 | | omelon 8426 |
. . . . . . 7
⊢ ω
∈ On |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ω ∈
On) |
34 | 1, 33, 2 | cantnff1o 8476 |
. . . . . . . . 9
⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴)) |
35 | | f1ocnv 6062 |
. . . . . . . . 9
⊢ ((ω
CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆) |
36 | | f1of 6050 |
. . . . . . . . 9
⊢ (◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
38 | 37, 3 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆) |
39 | 4, 38 | syl5eqel 2692 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
40 | 8 | oveq1i 6559 |
. . . . . . . . . 10
⊢ (𝑀 +𝑜 𝑧) = (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧) |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +𝑜 𝑧) = (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)) |
42 | 41 | mpt2eq3ia 6618 |
. . . . . . . 8
⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)) |
43 | | eqid 2610 |
. . . . . . . 8
⊢ ∅ =
∅ |
44 | | seqomeq12 7436 |
. . . . . . . 8
⊢ (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)) ∧ ∅ = ∅) →
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (𝑀
+𝑜 𝑧)),
∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅)) |
45 | 42, 43, 44 | mp2an 704 |
. . . . . . 7
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) |
46 | 6, 45 | eqtri 2632 |
. . . . . 6
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((ω ↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) |
47 | 1, 33, 2, 5, 39, 46 | cantnfval 8448 |
. . . . 5
⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = (𝐻‘dom 𝐺)) |
48 | 31, 47 | syl5reqr 2659 |
. . . 4
⊢ (𝜑 → (𝐻‘dom 𝐺) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))) |
49 | 18 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (𝐻‘dom 𝐺) = (𝐻‘suc ∪ dom
𝐺)) |
50 | | f1ocnvfv2 6433 |
. . . . 5
⊢
(((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) ∧ 𝐵 ∈ (ω ↑𝑜
𝐴)) → ((ω CNF
𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
51 | 34, 3, 50 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
52 | 48, 49, 51 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → (𝐻‘suc ∪ dom
𝐺) = 𝐵) |
53 | | f1oeq2 6041 |
. . 3
⊢ ((𝐻‘suc ∪ dom 𝐺) = 𝐵 → ((𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)) ↔ (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)))) |
54 | 52, 53 | syl 17 |
. 2
⊢ (𝜑 → ((𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)) ↔ (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊)))) |
55 | 30, 54 | mpbid 221 |
1
⊢ (𝜑 → (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))) |