Proof of Theorem cnfcom3clem
Step | Hyp | Ref
| Expression |
1 | | cnfcom3c.s |
. . . . . 6
⊢ 𝑆 = dom (ω CNF 𝐴) |
2 | | simp1 1138 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ∈ On) |
3 | | omelon 9261 |
. . . . . . . . 9
⊢ ω
∈ On |
4 | | 1onn 8367 |
. . . . . . . . 9
⊢
1o ∈ ω |
5 | | ondif2 8229 |
. . . . . . . . 9
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
6 | 3, 4, 5 | mpbir2an 711 |
. . . . . . . 8
⊢ ω
∈ (On ∖ 2o) |
7 | | oeworde 8321 |
. . . . . . . 8
⊢ ((ω
∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐴 ⊆ (ω ↑o 𝐴)) |
8 | 6, 2, 7 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ⊆ (ω ↑o 𝐴)) |
9 | | simp2 1139 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑏 ∈ 𝐴) |
10 | 8, 9 | sseldd 3902 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑏 ∈ (ω ↑o 𝐴)) |
11 | | cnfcom3c.f |
. . . . . 6
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝑏) |
12 | | cnfcom3c.g |
. . . . . 6
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
13 | | cnfcom3c.h |
. . . . . 6
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) |
14 | | cnfcom3c.t |
. . . . . 6
⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) |
15 | | cnfcom3c.m |
. . . . . 6
⊢ 𝑀 = ((ω ↑o
(𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) |
16 | | cnfcom3c.k |
. . . . . 6
⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) |
17 | | cnfcom3c.w |
. . . . . 6
⊢ 𝑊 = (𝐺‘∪ dom
𝐺) |
18 | | simp3 1140 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ω ⊆ 𝑏) |
19 | 1, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cnfcom3lem 9318 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑊 ∈ (On ∖
1o)) |
20 | | cnfcom3c.x |
. . . . . . 7
⊢ 𝑋 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((𝐹‘𝑊) ·o 𝑣) +o 𝑢)) |
21 | | cnfcom3c.y |
. . . . . . 7
⊢ 𝑌 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((ω
↑o 𝑊)
·o 𝑢)
+o 𝑣)) |
22 | | cnfcom3c.n |
. . . . . . 7
⊢ 𝑁 = ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)) |
23 | 1, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18, 20, 21, 22 | cnfcom3 9319 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏–1-1-onto→(ω ↑o 𝑊)) |
24 | | f1of 6661 |
. . . . . . . . . 10
⊢ (𝑁:𝑏–1-1-onto→(ω ↑o 𝑊) → 𝑁:𝑏⟶(ω ↑o 𝑊)) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏⟶(ω ↑o 𝑊)) |
26 | 25, 9 | fexd 7043 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁 ∈ V) |
27 | | cnfcom3c.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁) |
28 | 27 | fvmpt2 6829 |
. . . . . . . 8
⊢ ((𝑏 ∈ (ω
↑o 𝐴) ∧
𝑁 ∈ V) → (𝐿‘𝑏) = 𝑁) |
29 | 10, 26, 28 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏) = 𝑁) |
30 | 29 | f1oeq1d 6656 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊) ↔ 𝑁:𝑏–1-1-onto→(ω ↑o 𝑊))) |
31 | 23, 30 | mpbird 260 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) |
32 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (ω ↑o 𝑤) = (ω ↑o
𝑊)) |
33 | 32 | f1oeq3d 6658 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊))) |
34 | 33 | rspcev 3537 |
. . . . 5
⊢ ((𝑊 ∈ (On ∖
1o) ∧ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) |
35 | 19, 31, 34 | syl2anc 587 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) |
36 | 35 | 3expia 1123 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
37 | 36 | ralrimiva 3105 |
. 2
⊢ (𝐴 ∈ On → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
38 | | ovex 7246 |
. . . . 5
⊢ (ω
↑o 𝐴)
∈ V |
39 | 38 | mptex 7039 |
. . . 4
⊢ (𝑏 ∈ (ω
↑o 𝐴)
↦ 𝑁) ∈
V |
40 | 27, 39 | eqeltri 2834 |
. . 3
⊢ 𝐿 ∈ V |
41 | | nfmpt1 5153 |
. . . . . 6
⊢
Ⅎ𝑏(𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁) |
42 | 27, 41 | nfcxfr 2902 |
. . . . 5
⊢
Ⅎ𝑏𝐿 |
43 | 42 | nfeq2 2921 |
. . . 4
⊢
Ⅎ𝑏 𝑔 = 𝐿 |
44 | | fveq1 6716 |
. . . . . . 7
⊢ (𝑔 = 𝐿 → (𝑔‘𝑏) = (𝐿‘𝑏)) |
45 | 44 | f1oeq1d 6656 |
. . . . . 6
⊢ (𝑔 = 𝐿 → ((𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
46 | 45 | rexbidv 3216 |
. . . . 5
⊢ (𝑔 = 𝐿 → (∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
47 | 46 | imbi2d 344 |
. . . 4
⊢ (𝑔 = 𝐿 → ((ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) |
48 | 43, 47 | ralbid 3154 |
. . 3
⊢ (𝑔 = 𝐿 → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) |
49 | 40, 48 | spcev 3521 |
. 2
⊢
(∀𝑏 ∈
𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
50 | 37, 49 | syl 17 |
1
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |