Proof of Theorem cnfcom3
Step | Hyp | Ref
| Expression |
1 | | omelon 8543 |
. . . . . 6
⊢ ω
∈ On |
2 | | cnfcom.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ On) |
3 | | suppssdm 7308 |
. . . . . . . . 9
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
4 | | cnfcom.f |
. . . . . . . . . . . . 13
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) |
5 | | cnfcom.s |
. . . . . . . . . . . . . . . 16
⊢ 𝑆 = dom (ω CNF 𝐴) |
6 | 1 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ω ∈
On) |
7 | 5, 6, 2 | cantnff1o 8593 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴)) |
8 | | f1ocnv 6149 |
. . . . . . . . . . . . . . 15
⊢ ((ω
CNF 𝐴):𝑆–1-1-onto→(ω ↑𝑜 𝐴) → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆) |
9 | | f1of 6137 |
. . . . . . . . . . . . . . 15
⊢ (◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑𝑜 𝐴)⟶𝑆) |
11 | | cnfcom.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (ω ↑𝑜
𝐴)) |
12 | 10, 11 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆) |
13 | 4, 12 | syl5eqel 2705 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
14 | 5, 6, 2 | cantnfs 8563 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))) |
15 | 13, 14 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)) |
16 | 15 | simpld 475 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶ω) |
17 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶ω → dom 𝐹 = 𝐴) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
19 | 3, 18 | syl5sseq 3653 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴) |
20 | | cnfcom.w |
. . . . . . . . 9
⊢ 𝑊 = (𝐺‘∪ dom
𝐺) |
21 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 supp ∅) ∈
V |
22 | | cnfcom.g |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
23 | 22 | oion 8441 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 supp ∅) ∈ V →
dom 𝐺 ∈
On) |
24 | 21, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom 𝐺 ∈ On |
25 | 24 | elexi 3213 |
. . . . . . . . . . . . 13
⊢ dom 𝐺 ∈ V |
26 | 25 | uniex 6953 |
. . . . . . . . . . . 12
⊢ ∪ dom 𝐺 ∈ V |
27 | 26 | sucid 5804 |
. . . . . . . . . . 11
⊢ ∪ dom 𝐺 ∈ suc ∪ dom
𝐺 |
28 | | cnfcom.h |
. . . . . . . . . . . 12
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (𝑀
+𝑜 𝑧)),
∅) |
29 | | cnfcom.t |
. . . . . . . . . . . 12
⊢ 𝑇 =
seq𝜔((𝑘
∈ V, 𝑓 ∈ V
↦ 𝐾),
∅) |
30 | | cnfcom.m |
. . . . . . . . . . . 12
⊢ 𝑀 = ((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) |
31 | | cnfcom.k |
. . . . . . . . . . . 12
⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) |
32 | | cnfcom3.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ω ⊆ 𝐵) |
33 | | peano1 7085 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ ω |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∅ ∈
ω) |
35 | 32, 34 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∅ ∈ 𝐵) |
36 | 5, 2, 11, 4, 22, 28, 29, 30, 31, 20, 35 | cnfcom2lem 8598 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 = suc ∪ dom
𝐺) |
37 | 27, 36 | syl5eleqr 2708 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ dom 𝐺 ∈ dom 𝐺) |
38 | 22 | oif 8435 |
. . . . . . . . . . 11
⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅) |
39 | 38 | ffvelrni 6358 |
. . . . . . . . . 10
⊢ (∪ dom 𝐺 ∈ dom 𝐺 → (𝐺‘∪ dom
𝐺) ∈ (𝐹 supp ∅)) |
40 | 37, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘∪ dom
𝐺) ∈ (𝐹 supp ∅)) |
41 | 20, 40 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ (𝐹 supp ∅)) |
42 | 19, 41 | sseldd 3604 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ 𝐴) |
43 | | onelon 5748 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑊 ∈ 𝐴) → 𝑊 ∈ On) |
44 | 2, 42, 43 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ On) |
45 | | oecl 7617 |
. . . . . 6
⊢ ((ω
∈ On ∧ 𝑊 ∈
On) → (ω ↑𝑜 𝑊) ∈ On) |
46 | 1, 44, 45 | sylancr 695 |
. . . . 5
⊢ (𝜑 → (ω
↑𝑜 𝑊) ∈ On) |
47 | 16, 42 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑊) ∈ ω) |
48 | | nnon 7071 |
. . . . . 6
⊢ ((𝐹‘𝑊) ∈ ω → (𝐹‘𝑊) ∈ On) |
49 | 47, 48 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑊) ∈ On) |
50 | | cnfcom.y |
. . . . . 6
⊢ 𝑌 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑𝑜
𝑊) ↦ (((ω
↑𝑜 𝑊) ·𝑜 𝑢) +𝑜 𝑣)) |
51 | | cnfcom.x |
. . . . . 6
⊢ 𝑋 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑𝑜
𝑊) ↦ (((𝐹‘𝑊) ·𝑜 𝑣) +𝑜 𝑢)) |
52 | 50, 51 | omf1o 8063 |
. . . . 5
⊢
(((ω ↑𝑜 𝑊) ∈ On ∧ (𝐹‘𝑊) ∈ On) → (𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→((𝐹‘𝑊) ·𝑜 (ω
↑𝑜 𝑊))) |
53 | 46, 49, 52 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→((𝐹‘𝑊) ·𝑜 (ω
↑𝑜 𝑊))) |
54 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ω → 𝐹 Fn 𝐴) |
55 | 16, 54 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 Fn 𝐴) |
56 | | 0ex 4790 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
57 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∅ ∈
V) |
58 | | elsuppfn 7303 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V) →
(𝑊 ∈ (𝐹 supp ∅) ↔ (𝑊 ∈ 𝐴 ∧ (𝐹‘𝑊) ≠ ∅))) |
59 | 55, 2, 57, 58 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (𝑊 ∈ (𝐹 supp ∅) ↔ (𝑊 ∈ 𝐴 ∧ (𝐹‘𝑊) ≠ ∅))) |
60 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑊 ∈ 𝐴 ∧ (𝐹‘𝑊) ≠ ∅) → (𝐹‘𝑊) ≠ ∅) |
61 | 59, 60 | syl6bi 243 |
. . . . . . . 8
⊢ (𝜑 → (𝑊 ∈ (𝐹 supp ∅) → (𝐹‘𝑊) ≠ ∅)) |
62 | 41, 61 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑊) ≠ ∅) |
63 | | on0eln0 5780 |
. . . . . . . 8
⊢ ((𝐹‘𝑊) ∈ On → (∅ ∈ (𝐹‘𝑊) ↔ (𝐹‘𝑊) ≠ ∅)) |
64 | 47, 48, 63 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (∅ ∈ (𝐹‘𝑊) ↔ (𝐹‘𝑊) ≠ ∅)) |
65 | 62, 64 | mpbird 247 |
. . . . . 6
⊢ (𝜑 → ∅ ∈ (𝐹‘𝑊)) |
66 | 5, 2, 11, 4, 22, 28, 29, 30, 31, 20, 32 | cnfcom3lem 8600 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ (On ∖
1𝑜)) |
67 | | ondif1 7581 |
. . . . . . . 8
⊢ (𝑊 ∈ (On ∖
1𝑜) ↔ (𝑊 ∈ On ∧ ∅ ∈ 𝑊)) |
68 | 67 | simprbi 480 |
. . . . . . 7
⊢ (𝑊 ∈ (On ∖
1𝑜) → ∅ ∈ 𝑊) |
69 | 66, 68 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∅ ∈ 𝑊) |
70 | | omabs 7727 |
. . . . . 6
⊢ ((((𝐹‘𝑊) ∈ ω ∧ ∅ ∈ (𝐹‘𝑊)) ∧ (𝑊 ∈ On ∧ ∅ ∈ 𝑊)) → ((𝐹‘𝑊) ·𝑜 (ω
↑𝑜 𝑊)) = (ω ↑𝑜
𝑊)) |
71 | 47, 65, 44, 69, 70 | syl22anc 1327 |
. . . . 5
⊢ (𝜑 → ((𝐹‘𝑊) ·𝑜 (ω
↑𝑜 𝑊)) = (ω ↑𝑜
𝑊)) |
72 | | f1oeq3 6129 |
. . . . 5
⊢ (((𝐹‘𝑊) ·𝑜 (ω
↑𝑜 𝑊)) = (ω ↑𝑜
𝑊) → ((𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→((𝐹‘𝑊) ·𝑜 (ω
↑𝑜 𝑊)) ↔ (𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→(ω ↑𝑜 𝑊))) |
73 | 71, 72 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→((𝐹‘𝑊) ·𝑜 (ω
↑𝑜 𝑊)) ↔ (𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→(ω ↑𝑜 𝑊))) |
74 | 53, 73 | mpbid 222 |
. . 3
⊢ (𝜑 → (𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→(ω ↑𝑜 𝑊)) |
75 | 5, 2, 11, 4, 22, 28, 29, 30, 31, 20, 35 | cnfcom2 8599 |
. . 3
⊢ (𝜑 → (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))) |
76 | | f1oco 6159 |
. . 3
⊢ (((𝑋 ∘ ◡𝑌):((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))–1-1-onto→(ω ↑𝑜 𝑊) ∧ (𝑇‘dom 𝐺):𝐵–1-1-onto→((ω ↑𝑜 𝑊) ·𝑜
(𝐹‘𝑊))) → ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)):𝐵–1-1-onto→(ω ↑𝑜 𝑊)) |
77 | 74, 75, 76 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)):𝐵–1-1-onto→(ω ↑𝑜 𝑊)) |
78 | | cnfcom.n |
. . 3
⊢ 𝑁 = ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)) |
79 | | f1oeq1 6127 |
. . 3
⊢ (𝑁 = ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)) → (𝑁:𝐵–1-1-onto→(ω ↑𝑜 𝑊) ↔ ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)):𝐵–1-1-onto→(ω ↑𝑜 𝑊))) |
80 | 78, 79 | ax-mp 5 |
. 2
⊢ (𝑁:𝐵–1-1-onto→(ω ↑𝑜 𝑊) ↔ ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)):𝐵–1-1-onto→(ω ↑𝑜 𝑊)) |
81 | 77, 80 | sylibr 224 |
1
⊢ (𝜑 → 𝑁:𝐵–1-1-onto→(ω ↑𝑜 𝑊)) |