Step | Hyp | Ref
| Expression |
1 | | ctex 8753 |
. 2
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
2 | | pwexr 7615 |
. 2
⊢
(𝒫 𝑋 ∈
2ndω → 𝑋 ∈ V) |
3 | | snex 5354 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
4 | 3 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 → {𝑥} ∈ V)) |
5 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
6 | 5 | sneqr 4771 |
. . . . . . . . 9
⊢ ({𝑥} = {𝑦} → 𝑥 = 𝑦) |
7 | | sneq 4571 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
8 | 6, 7 | impbii 208 |
. . . . . . . 8
⊢ ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦) |
9 | 8 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦))) |
10 | 4, 9 | dom2lem 8780 |
. . . . . 6
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V) |
11 | | f1f1orn 6727 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
13 | | f1oeng 8759 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
14 | 12, 13 | mpdan 684 |
. . . 4
⊢ (𝑋 ∈ V → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
15 | | domen1 8906 |
. . . 4
⊢ (𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) → (𝑋 ≼ ω ↔ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔ ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
17 | | distop 22145 |
. . . . . . 7
⊢ (𝑋 ∈ V → 𝒫 𝑋 ∈ Top) |
18 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
19 | 5 | snelpw 5361 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↔ {𝑥} ∈ 𝒫 𝑋) |
20 | 18, 19 | sylib 217 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
21 | 20 | fmpttd 6989 |
. . . . . . . 8
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋) |
22 | 21 | frnd 6608 |
. . . . . . 7
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋) |
23 | | elpwi 4542 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
24 | 23 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑦 ⊆ 𝑋) |
25 | | simprr 770 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑦) |
26 | 24, 25 | sseldd 3922 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑋) |
27 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} = {𝑧}) |
28 | | sneq 4571 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
29 | 28 | rspceeqv 3575 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ {𝑧} = {𝑧}) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
30 | 26, 27, 29 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
31 | | snex 5354 |
. . . . . . . . . . 11
⊢ {𝑧} ∈ V |
32 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 ↦ {𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑥}) |
33 | 32 | elrnmpt 5865 |
. . . . . . . . . . 11
⊢ ({𝑧} ∈ V → ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥})) |
34 | 31, 33 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
35 | 30, 34 | sylibr 233 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
36 | | vsnid 4598 |
. . . . . . . . . 10
⊢ 𝑧 ∈ {𝑧} |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ {𝑧}) |
38 | 25 | snssd 4742 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ⊆ 𝑦) |
39 | | eleq2 2827 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ {𝑧})) |
40 | | sseq1 3946 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑤 ⊆ 𝑦 ↔ {𝑧} ⊆ 𝑦)) |
41 | 39, 40 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑧} → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) ↔ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦))) |
42 | 41 | rspcev 3561 |
. . . . . . . . 9
⊢ (({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∧ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
43 | 35, 37, 38, 42 | syl12anc 834 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
44 | 43 | ralrimivva 3123 |
. . . . . . 7
⊢ (𝑋 ∈ V → ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
45 | | basgen2 22139 |
. . . . . . 7
⊢
((𝒫 𝑋 ∈
Top ∧ ran (𝑥 ∈
𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) → (topGen‘ran (𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
46 | 17, 22, 44, 45 | syl3anc 1370 |
. . . . . 6
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
47 | 46 | adantr 481 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
48 | 46, 17 | eqeltrd 2839 |
. . . . . . 7
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) ∈ Top) |
49 | | tgclb 22120 |
. . . . . . 7
⊢ (ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ↔ (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈ Top) |
50 | 48, 49 | sylibr 233 |
. . . . . 6
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases) |
51 | | 2ndci 22599 |
. . . . . 6
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2ndω) |
52 | 50, 51 | sylan 580 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2ndω) |
53 | 47, 52 | eqeltrrd 2840 |
. . . 4
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → 𝒫 𝑋 ∈
2ndω) |
54 | | is2ndc 22597 |
. . . . . 6
⊢
(𝒫 𝑋 ∈
2ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) |
55 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
56 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
57 | 56, 19 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
58 | | simplrr 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → (topGen‘𝑏) = 𝒫 𝑋) |
59 | 57, 58 | eleqtrrd 2842 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ (topGen‘𝑏)) |
60 | | vsnid 4598 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ {𝑥} |
61 | | tg2 22115 |
. . . . . . . . . . . . 13
⊢ (({𝑥} ∈ (topGen‘𝑏) ∧ 𝑥 ∈ {𝑥}) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
62 | 59, 60, 61 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
63 | | simprrl 778 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑥 ∈ 𝑦) |
64 | 63 | snssd 4742 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ⊆ 𝑦) |
65 | | simprrr 779 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ⊆ {𝑥}) |
66 | 64, 65 | eqssd 3938 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} = 𝑦) |
67 | | simprl 768 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ∈ 𝑏) |
68 | 66, 67 | eqeltrd 2839 |
. . . . . . . . . . . 12
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ∈ 𝑏) |
69 | 62, 68 | rexlimddv 3220 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝑏) |
70 | 69 | fmpttd 6989 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝑏) |
71 | 70 | frnd 6608 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏) |
72 | | ssdomg 8786 |
. . . . . . . . 9
⊢ (𝑏 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏)) |
73 | 55, 71, 72 | mpsyl 68 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏) |
74 | | simprl 768 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → 𝑏 ≼
ω) |
75 | | domtr 8793 |
. . . . . . . 8
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏 ∧ 𝑏 ≼ ω) → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
76 | 73, 74, 75 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
77 | 76 | rexlimdva2 3216 |
. . . . . 6
⊢ (𝑋 ∈ V → (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
78 | 54, 77 | syl5bi 241 |
. . . . 5
⊢ (𝑋 ∈ V → (𝒫
𝑋 ∈
2ndω → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
79 | 78 | imp 407 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2ndω)
→ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
80 | 53, 79 | impbida 798 |
. . 3
⊢ (𝑋 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω ↔ 𝒫 𝑋 ∈
2ndω)) |
81 | 16, 80 | bitrd 278 |
. 2
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2ndω)) |
82 | 1, 2, 81 | pm5.21nii 380 |
1
⊢ (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2ndω) |