Proof of Theorem cnfcom2
Step | Hyp | Ref
| Expression |
1 | | cnfcom.s |
. . . . 5
⊢ 𝑆 = dom (ω CNF 𝐴) |
2 | | cnfcom.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ On) |
3 | | cnfcom.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴)) |
4 | | cnfcom.f |
. . . . 5
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) |
5 | | cnfcom.g |
. . . . 5
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
6 | | cnfcom.h |
. . . . 5
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) |
7 | | cnfcom.t |
. . . . 5
⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) |
8 | | cnfcom.m |
. . . . 5
⊢ 𝑀 = ((ω ↑o
(𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) |
9 | | cnfcom.k |
. . . . 5
⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) |
10 | | ovex 7437 |
. . . . . . . . . 10
⊢ (𝐹 supp ∅) ∈
V |
11 | 5 | oion 9527 |
. . . . . . . . . 10
⊢ ((𝐹 supp ∅) ∈ V →
dom 𝐺 ∈
On) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢ dom 𝐺 ∈ On |
13 | 12 | elexi 3494 |
. . . . . . . 8
⊢ dom 𝐺 ∈ V |
14 | 13 | uniex 7726 |
. . . . . . 7
⊢ ∪ dom 𝐺 ∈ V |
15 | 14 | sucid 6443 |
. . . . . 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 9692 |
. . . . . 6
⊢ (𝜑 → dom 𝐺 = suc ∪ dom
𝐺) |
19 | 15, 18 | eleqtrrid 2841 |
. . . . 5
⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺) |
20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 19 | cnfcom 9691 |
. . . 4
⊢ (𝜑 → (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o (𝐺‘∪ dom 𝐺)) ·o (𝐹‘(𝐺‘∪ dom
𝐺)))) |
21 | 16 | oveq2i 7415 |
. . . . . 6
⊢ (ω
↑o 𝑊) =
(ω ↑o (𝐺‘∪ dom
𝐺)) |
22 | 16 | fveq2i 6891 |
. . . . . 6
⊢ (𝐹‘𝑊) = (𝐹‘(𝐺‘∪ dom
𝐺)) |
23 | 21, 22 | oveq12i 7416 |
. . . . 5
⊢ ((ω
↑o 𝑊)
·o (𝐹‘𝑊)) = ((ω ↑o (𝐺‘∪ dom 𝐺)) ·o (𝐹‘(𝐺‘∪ dom
𝐺))) |
24 | | f1oeq3 6820 |
. . . . 5
⊢
(((ω ↑o 𝑊) ·o (𝐹‘𝑊)) = ((ω ↑o (𝐺‘∪ dom 𝐺)) ·o (𝐹‘(𝐺‘∪ dom
𝐺))) → ((𝑇‘suc ∪ dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊)) ↔ (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o (𝐺‘∪ dom 𝐺)) ·o (𝐹‘(𝐺‘∪ dom
𝐺))))) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢ ((𝑇‘suc ∪ dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊)) ↔ (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o (𝐺‘∪ dom 𝐺)) ·o (𝐹‘(𝐺‘∪ dom
𝐺)))) |
26 | 20, 25 | sylibr 233 |
. . 3
⊢ (𝜑 → (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊))) |
27 | 18 | fveq2d 6892 |
. . . 4
⊢ (𝜑 → (𝑇‘dom 𝐺) = (𝑇‘suc ∪ dom
𝐺)) |
28 | 27 | f1oeq1d 6825 |
. . 3
⊢ (𝜑 → ((𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊)) ↔ (𝑇‘suc ∪ dom
𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊)))) |
29 | 26, 28 | mpbird 257 |
. 2
⊢ (𝜑 → (𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊))) |
30 | | omelon 9637 |
. . . . . . 7
⊢ ω
∈ On |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ω ∈
On) |
32 | 1, 31, 2 | cantnff1o 9687 |
. . . . . . . . 9
⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴)) |
33 | | f1ocnv 6842 |
. . . . . . . . 9
⊢ ((ω
CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆) |
34 | | f1of 6830 |
. . . . . . . . 9
⊢ (◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆) |
36 | 35, 3 | ffvelcdmd 7083 |
. . . . . . 7
⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆) |
37 | 4, 36 | eqeltrid 2838 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
38 | 8 | oveq1i 7414 |
. . . . . . . . . 10
⊢ (𝑀 +o 𝑧) = (((ω
↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧) |
39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑘 ∈ V ∧ 𝑧 ∈ V) → (𝑀 +o 𝑧) = (((ω
↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) |
40 | 39 | mpoeq3ia 7482 |
. . . . . . . 8
⊢ (𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) |
41 | | eqid 2733 |
. . . . . . . 8
⊢ ∅ =
∅ |
42 | | seqomeq12 8449 |
. . . . . . . 8
⊢ (((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)) = (𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ∧ ∅ = ∅) →
seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (𝑀 +o
𝑧)), ∅) =
seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)) |
43 | 40, 41, 42 | mp2an 691 |
. . . . . . 7
⊢
seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅) |
44 | 6, 43 | eqtri 2761 |
. . . . . 6
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅) |
45 | 1, 31, 2, 5, 37, 44 | cantnfval 9659 |
. . . . 5
⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = (𝐻‘dom 𝐺)) |
46 | 4 | fveq2i 6891 |
. . . . 5
⊢ ((ω
CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) |
47 | 45, 46 | eqtr3di 2788 |
. . . 4
⊢ (𝜑 → (𝐻‘dom 𝐺) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))) |
48 | 18 | fveq2d 6892 |
. . . 4
⊢ (𝜑 → (𝐻‘dom 𝐺) = (𝐻‘suc ∪ dom
𝐺)) |
49 | | f1ocnvfv2 7270 |
. . . . 5
⊢
(((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) ∧ 𝐵 ∈ (ω ↑o 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
50 | 32, 3, 49 | syl2anc 585 |
. . . 4
⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵) |
51 | 47, 48, 50 | 3eqtr3d 2781 |
. . 3
⊢ (𝜑 → (𝐻‘suc ∪ dom
𝐺) = 𝐵) |
52 | 51 | f1oeq2d 6826 |
. 2
⊢ (𝜑 → ((𝑇‘dom 𝐺):(𝐻‘suc ∪ dom
𝐺)–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊)) ↔ (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊)))) |
53 | 29, 52 | mpbid 231 |
1
⊢ (𝜑 → (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑o 𝑊) ·o (𝐹‘𝑊))) |