Proof of Theorem cnfcom3clem
Step | Hyp | Ref
| Expression |
1 | | cnfcom3c.s |
. . . . . 6
⊢ 𝑆 = dom (ω CNF 𝐴) |
2 | | simp1 1132 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ∈ On) |
3 | | omelon 9103 |
. . . . . . . . 9
⊢ ω
∈ On |
4 | | 1onn 8259 |
. . . . . . . . 9
⊢
1o ∈ ω |
5 | | ondif2 8121 |
. . . . . . . . 9
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
6 | 3, 4, 5 | mpbir2an 709 |
. . . . . . . 8
⊢ ω
∈ (On ∖ 2o) |
7 | | oeworde 8213 |
. . . . . . . 8
⊢ ((ω
∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐴 ⊆ (ω ↑o 𝐴)) |
8 | 6, 2, 7 | sylancr 589 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ⊆ (ω ↑o 𝐴)) |
9 | | simp2 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑏 ∈ 𝐴) |
10 | 8, 9 | sseldd 3967 |
. . . . . 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 1134 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ω ⊆ 𝑏) |
19 | 1, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cnfcom3lem 9160 |
. . . . 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 9161 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏–1-1-onto→(ω ↑o 𝑊)) |
24 | | f1of 6609 |
. . . . . . . . . 10
⊢ (𝑁:𝑏–1-1-onto→(ω ↑o 𝑊) → 𝑁:𝑏⟶(ω ↑o 𝑊)) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏⟶(ω ↑o 𝑊)) |
26 | | vex 3497 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
27 | | fex 6983 |
. . . . . . . . 9
⊢ ((𝑁:𝑏⟶(ω ↑o 𝑊) ∧ 𝑏 ∈ V) → 𝑁 ∈ V) |
28 | 25, 26, 27 | sylancl 588 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁 ∈ V) |
29 | | cnfcom3c.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁) |
30 | 29 | fvmpt2 6773 |
. . . . . . . 8
⊢ ((𝑏 ∈ (ω
↑o 𝐴) ∧
𝑁 ∈ V) → (𝐿‘𝑏) = 𝑁) |
31 | 10, 28, 30 | syl2anc 586 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏) = 𝑁) |
32 | | f1oeq1 6598 |
. . . . . . 7
⊢ ((𝐿‘𝑏) = 𝑁 → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊) ↔ 𝑁:𝑏–1-1-onto→(ω ↑o 𝑊))) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊) ↔ 𝑁:𝑏–1-1-onto→(ω ↑o 𝑊))) |
34 | 23, 33 | mpbird 259 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) |
35 | | oveq2 7158 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (ω ↑o 𝑤) = (ω ↑o
𝑊)) |
36 | 35 | f1oeq3d 6606 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊))) |
37 | 36 | rspcev 3622 |
. . . . 5
⊢ ((𝑊 ∈ (On ∖
1o) ∧ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) |
38 | 19, 34, 37 | syl2anc 586 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) |
39 | 38 | 3expia 1117 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
40 | 39 | ralrimiva 3182 |
. 2
⊢ (𝐴 ∈ On → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
41 | | ovex 7183 |
. . . . 5
⊢ (ω
↑o 𝐴)
∈ V |
42 | 41 | mptex 6980 |
. . . 4
⊢ (𝑏 ∈ (ω
↑o 𝐴)
↦ 𝑁) ∈
V |
43 | 29, 42 | eqeltri 2909 |
. . 3
⊢ 𝐿 ∈ V |
44 | | nfmpt1 5156 |
. . . . . 6
⊢
Ⅎ𝑏(𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁) |
45 | 29, 44 | nfcxfr 2975 |
. . . . 5
⊢
Ⅎ𝑏𝐿 |
46 | 45 | nfeq2 2995 |
. . . 4
⊢
Ⅎ𝑏 𝑔 = 𝐿 |
47 | | fveq1 6663 |
. . . . . . 7
⊢ (𝑔 = 𝐿 → (𝑔‘𝑏) = (𝐿‘𝑏)) |
48 | | f1oeq1 6598 |
. . . . . . 7
⊢ ((𝑔‘𝑏) = (𝐿‘𝑏) → ((𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
49 | 47, 48 | syl 17 |
. . . . . 6
⊢ (𝑔 = 𝐿 → ((𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
50 | 49 | rexbidv 3297 |
. . . . 5
⊢ (𝑔 = 𝐿 → (∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
51 | 50 | imbi2d 343 |
. . . 4
⊢ (𝑔 = 𝐿 → ((ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) |
52 | 46, 51 | ralbid 3231 |
. . 3
⊢ (𝑔 = 𝐿 → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) |
53 | 43, 52 | spcev 3606 |
. 2
⊢
(∀𝑏 ∈
𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
54 | 40, 53 | syl 17 |
1
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |