Proof of Theorem cnfcom3clem
Step | Hyp | Ref
| Expression |
1 | | cnfcom3c.s |
. . . . . 6
⊢ 𝑆 = dom (ω CNF 𝐴) |
2 | | simp1 1116 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ∈ On) |
3 | | omelon 8903 |
. . . . . . . . 9
⊢ ω
∈ On |
4 | | 1onn 8066 |
. . . . . . . . 9
⊢
1o ∈ ω |
5 | | ondif2 7929 |
. . . . . . . . 9
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
6 | 3, 4, 5 | mpbir2an 698 |
. . . . . . . 8
⊢ ω
∈ (On ∖ 2o) |
7 | | oeworde 8020 |
. . . . . . . 8
⊢ ((ω
∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐴 ⊆ (ω ↑o 𝐴)) |
8 | 6, 2, 7 | sylancr 578 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ⊆ (ω ↑o 𝐴)) |
9 | | simp2 1117 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑏 ∈ 𝐴) |
10 | 8, 9 | sseldd 3859 |
. . . . . 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 1118 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ω ⊆ 𝑏) |
19 | 1, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cnfcom3lem 8960 |
. . . . 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 8961 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏–1-1-onto→(ω ↑o 𝑊)) |
24 | | f1of 6444 |
. . . . . . . . . 10
⊢ (𝑁:𝑏–1-1-onto→(ω ↑o 𝑊) → 𝑁:𝑏⟶(ω ↑o 𝑊)) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏⟶(ω ↑o 𝑊)) |
26 | | vex 3418 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
27 | | fex 6815 |
. . . . . . . . 9
⊢ ((𝑁:𝑏⟶(ω ↑o 𝑊) ∧ 𝑏 ∈ V) → 𝑁 ∈ V) |
28 | 25, 26, 27 | sylancl 577 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁 ∈ V) |
29 | | cnfcom3c.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁) |
30 | 29 | fvmpt2 6605 |
. . . . . . . 8
⊢ ((𝑏 ∈ (ω
↑o 𝐴) ∧
𝑁 ∈ V) → (𝐿‘𝑏) = 𝑁) |
31 | 10, 28, 30 | syl2anc 576 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏) = 𝑁) |
32 | | f1oeq1 6433 |
. . . . . . 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 249 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) |
35 | | oveq2 6984 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (ω ↑o 𝑤) = (ω ↑o
𝑊)) |
36 | 35 | f1oeq3d 6441 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊))) |
37 | 36 | rspcev 3535 |
. . . . 5
⊢ ((𝑊 ∈ (On ∖
1o) ∧ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) |
38 | 19, 34, 37 | syl2anc 576 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) |
39 | 38 | 3expia 1101 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
40 | 39 | ralrimiva 3132 |
. 2
⊢ (𝐴 ∈ On → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
41 | | ovex 7008 |
. . . . 5
⊢ (ω
↑o 𝐴)
∈ V |
42 | 41 | mptex 6812 |
. . . 4
⊢ (𝑏 ∈ (ω
↑o 𝐴)
↦ 𝑁) ∈
V |
43 | 29, 42 | eqeltri 2862 |
. . 3
⊢ 𝐿 ∈ V |
44 | | nfmpt1 5025 |
. . . . . 6
⊢
Ⅎ𝑏(𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁) |
45 | 29, 44 | nfcxfr 2930 |
. . . . 5
⊢
Ⅎ𝑏𝐿 |
46 | 45 | nfeq2 2947 |
. . . 4
⊢
Ⅎ𝑏 𝑔 = 𝐿 |
47 | | fveq1 6498 |
. . . . . . 7
⊢ (𝑔 = 𝐿 → (𝑔‘𝑏) = (𝐿‘𝑏)) |
48 | | f1oeq1 6433 |
. . . . . . 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 3242 |
. . . . 5
⊢ (𝑔 = 𝐿 → (∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
51 | 50 | imbi2d 333 |
. . . 4
⊢ (𝑔 = 𝐿 → ((ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) |
52 | 46, 51 | ralbid 3178 |
. . 3
⊢ (𝑔 = 𝐿 → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) |
53 | 43, 52 | spcev 3525 |
. 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 𝑤))) |