Proof of Theorem cnfcom3clem
Step | Hyp | Ref
| Expression |
1 | | cnfcom3c.s |
. . . . . 6
⊢ 𝑆 = dom (ω CNF 𝐴) |
2 | | simp1 1054 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ∈ On) |
3 | | omelon 8426 |
. . . . . . . . 9
⊢ ω
∈ On |
4 | | 1onn 7606 |
. . . . . . . . 9
⊢
1𝑜 ∈ ω |
5 | | ondif2 7469 |
. . . . . . . . 9
⊢ (ω
∈ (On ∖ 2𝑜) ↔ (ω ∈ On ∧
1𝑜 ∈ ω)) |
6 | 3, 4, 5 | mpbir2an 957 |
. . . . . . . 8
⊢ ω
∈ (On ∖ 2𝑜) |
7 | | oeworde 7560 |
. . . . . . . 8
⊢ ((ω
∈ (On ∖ 2𝑜) ∧ 𝐴 ∈ On) → 𝐴 ⊆ (ω ↑𝑜
𝐴)) |
8 | 6, 2, 7 | sylancr 694 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ⊆ (ω ↑𝑜
𝐴)) |
9 | | simp2 1055 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑏 ∈ 𝐴) |
10 | 8, 9 | sseldd 3569 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑏 ∈ (ω ↑𝑜
𝐴)) |
11 | | cnfcom3c.f |
. . . . . 6
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝑏) |
12 | | cnfcom3c.g |
. . . . . 6
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
13 | | cnfcom3c.h |
. . . . . 6
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (𝑀
+𝑜 𝑧)),
∅) |
14 | | cnfcom3c.t |
. . . . . 6
⊢ 𝑇 =
seq𝜔((𝑘
∈ V, 𝑓 ∈ V
↦ 𝐾),
∅) |
15 | | cnfcom3c.m |
. . . . . 6
⊢ 𝑀 = ((ω
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) |
16 | | cnfcom3c.k |
. . . . . 6
⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +𝑜 𝑥))) |
17 | | cnfcom3c.w |
. . . . . 6
⊢ 𝑊 = (𝐺‘∪ dom
𝐺) |
18 | | simp3 1056 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ω ⊆ 𝑏) |
19 | 1, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cnfcom3lem 8483 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑊 ∈ (On ∖
1𝑜)) |
20 | | cnfcom3c.x |
. . . . . . 7
⊢ 𝑋 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑𝑜
𝑊) ↦ (((𝐹‘𝑊) ·𝑜 𝑣) +𝑜 𝑢)) |
21 | | cnfcom3c.y |
. . . . . . 7
⊢ 𝑌 = (𝑢 ∈ (𝐹‘𝑊), 𝑣 ∈ (ω ↑𝑜
𝑊) ↦ (((ω
↑𝑜 𝑊) ·𝑜 𝑢) +𝑜 𝑣)) |
22 | | cnfcom3c.n |
. . . . . . 7
⊢ 𝑁 = ((𝑋 ∘ ◡𝑌) ∘ (𝑇‘dom 𝐺)) |
23 | 1, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18, 20, 21, 22 | cnfcom3 8484 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏–1-1-onto→(ω ↑𝑜 𝑊)) |
24 | | f1of 6050 |
. . . . . . . . . 10
⊢ (𝑁:𝑏–1-1-onto→(ω ↑𝑜 𝑊) → 𝑁:𝑏⟶(ω ↑𝑜
𝑊)) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏⟶(ω ↑𝑜
𝑊)) |
26 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
27 | | fex 6394 |
. . . . . . . . 9
⊢ ((𝑁:𝑏⟶(ω ↑𝑜
𝑊) ∧ 𝑏 ∈ V) → 𝑁 ∈ V) |
28 | 25, 26, 27 | sylancl 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → 𝑁 ∈ V) |
29 | | cnfcom3c.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑏 ∈ (ω ↑𝑜
𝐴) ↦ 𝑁) |
30 | 29 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑏 ∈ (ω
↑𝑜 𝐴) ∧ 𝑁 ∈ V) → (𝐿‘𝑏) = 𝑁) |
31 | 10, 28, 30 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏) = 𝑁) |
32 | | f1oeq1 6040 |
. . . . . . 7
⊢ ((𝐿‘𝑏) = 𝑁 → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊) ↔ 𝑁:𝑏–1-1-onto→(ω ↑𝑜 𝑊))) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊) ↔ 𝑁:𝑏–1-1-onto→(ω ↑𝑜 𝑊))) |
34 | 23, 33 | mpbird 246 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊)) |
35 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (ω ↑𝑜
𝑤) = (ω
↑𝑜 𝑊)) |
36 | | f1oeq3 6042 |
. . . . . . 7
⊢ ((ω
↑𝑜 𝑤) = (ω ↑𝑜 𝑊) → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊))) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊))) |
38 | 37 | rspcev 3282 |
. . . . 5
⊢ ((𝑊 ∈ (On ∖
1𝑜) ∧ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊)) → ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)) |
39 | 19, 34, 38 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏) → ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)) |
40 | 39 | 3expia 1259 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
41 | 40 | ralrimiva 2949 |
. 2
⊢ (𝐴 ∈ On → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
42 | | ovex 6577 |
. . . . 5
⊢ (ω
↑𝑜 𝐴) ∈ V |
43 | 42 | mptex 6390 |
. . . 4
⊢ (𝑏 ∈ (ω
↑𝑜 𝐴) ↦ 𝑁) ∈ V |
44 | 29, 43 | eqeltri 2684 |
. . 3
⊢ 𝐿 ∈ V |
45 | | nfmpt1 4675 |
. . . . . 6
⊢
Ⅎ𝑏(𝑏 ∈ (ω ↑𝑜
𝐴) ↦ 𝑁) |
46 | 29, 45 | nfcxfr 2749 |
. . . . 5
⊢
Ⅎ𝑏𝐿 |
47 | 46 | nfeq2 2766 |
. . . 4
⊢
Ⅎ𝑏 𝑔 = 𝐿 |
48 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑔 = 𝐿 → (𝑔‘𝑏) = (𝐿‘𝑏)) |
49 | | f1oeq1 6040 |
. . . . . . 7
⊢ ((𝑔‘𝑏) = (𝐿‘𝑏) → ((𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
50 | 48, 49 | syl 17 |
. . . . . 6
⊢ (𝑔 = 𝐿 → ((𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
51 | 50 | rexbidv 3034 |
. . . . 5
⊢ (𝑔 = 𝐿 → (∃𝑤 ∈ (On ∖
1𝑜)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤) ↔ ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
52 | 51 | imbi2d 329 |
. . . 4
⊢ (𝑔 = 𝐿 → ((ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)))) |
53 | 47, 52 | ralbid 2966 |
. . 3
⊢ (𝑔 = 𝐿 → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)))) |
54 | 44, 53 | spcev 3273 |
. 2
⊢
(∀𝑏 ∈
𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝐿‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
55 | 41, 54 | syl 17 |
1
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |