Step | Hyp | Ref
| Expression |
1 | | reldom 7961 |
. . 3
⊢ Rel
≼ |
2 | 1 | brrelexi 5158 |
. 2
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
3 | | pwexr 6974 |
. 2
⊢
(𝒫 𝑋 ∈
2nd𝜔 → 𝑋 ∈ V) |
4 | | elex 3212 |
. . . . 5
⊢ (𝑋 ∈ V → 𝑋 ∈ V) |
5 | | snex 4908 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
6 | 5 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 → {𝑥} ∈ V)) |
7 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
8 | 7 | sneqr 4371 |
. . . . . . . . 9
⊢ ({𝑥} = {𝑦} → 𝑥 = 𝑦) |
9 | | sneq 4187 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
10 | 8, 9 | impbii 199 |
. . . . . . . 8
⊢ ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦) |
11 | 10 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦))) |
12 | 6, 11 | dom2lem 7995 |
. . . . . 6
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V) |
13 | | f1f1orn 6148 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
15 | | f1oeng 7974 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
16 | 4, 14, 15 | syl2anc 693 |
. . . 4
⊢ (𝑋 ∈ V → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
17 | | domen1 8102 |
. . . 4
⊢ (𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) → (𝑋 ≼ ω ↔ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔ ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
19 | | distop 20799 |
. . . . . . 7
⊢ (𝑋 ∈ V → 𝒫 𝑋 ∈ Top) |
20 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
21 | 7 | snelpw 4913 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↔ {𝑥} ∈ 𝒫 𝑋) |
22 | 20, 21 | sylib 208 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
23 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ {𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑥}) |
24 | 22, 23 | fmptd 6385 |
. . . . . . . 8
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋) |
25 | | frn 6053 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋) |
27 | | elpwi 4168 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
28 | 27 | ad2antrl 764 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑦 ⊆ 𝑋) |
29 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑦) |
30 | 28, 29 | sseldd 3604 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑋) |
31 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} = {𝑧}) |
32 | | sneq 4187 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
33 | 32 | eqeq2d 2632 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ({𝑧} = {𝑥} ↔ {𝑧} = {𝑧})) |
34 | 33 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ {𝑧} = {𝑧}) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
35 | 30, 31, 34 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
36 | | snex 4908 |
. . . . . . . . . . 11
⊢ {𝑧} ∈ V |
37 | 23 | elrnmpt 5372 |
. . . . . . . . . . 11
⊢ ({𝑧} ∈ V → ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥})) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
39 | 35, 38 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
40 | | vsnid 4209 |
. . . . . . . . . 10
⊢ 𝑧 ∈ {𝑧} |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ {𝑧}) |
42 | 29 | snssd 4340 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ⊆ 𝑦) |
43 | | eleq2 2690 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ {𝑧})) |
44 | | sseq1 3626 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑤 ⊆ 𝑦 ↔ {𝑧} ⊆ 𝑦)) |
45 | 43, 44 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑧} → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) ↔ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦))) |
46 | 45 | rspcev 3309 |
. . . . . . . . 9
⊢ (({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∧ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
47 | 39, 41, 42, 46 | syl12anc 1324 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
48 | 47 | ralrimivva 2971 |
. . . . . . 7
⊢ (𝑋 ∈ V → ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
49 | | basgen2 20793 |
. . . . . . 7
⊢
((𝒫 𝑋 ∈
Top ∧ ran (𝑥 ∈
𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) → (topGen‘ran (𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
50 | 19, 26, 48, 49 | syl3anc 1326 |
. . . . . 6
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
51 | 50 | adantr 481 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
52 | 50, 19 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) ∈ Top) |
53 | | tgclb 20774 |
. . . . . . 7
⊢ (ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ↔ (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈ Top) |
54 | 52, 53 | sylibr 224 |
. . . . . 6
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases) |
55 | | 2ndci 21251 |
. . . . . 6
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2nd𝜔) |
56 | 54, 55 | sylan 488 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2nd𝜔) |
57 | 51, 56 | eqeltrrd 2702 |
. . . 4
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → 𝒫 𝑋 ∈
2nd𝜔) |
58 | | is2ndc 21249 |
. . . . . 6
⊢
(𝒫 𝑋 ∈
2nd𝜔 ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) |
59 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
60 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
61 | 60, 21 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
62 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → (topGen‘𝑏) = 𝒫 𝑋) |
63 | 61, 62 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ (topGen‘𝑏)) |
64 | | vsnid 4209 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ {𝑥} |
65 | | tg2 20769 |
. . . . . . . . . . . . . 14
⊢ (({𝑥} ∈ (topGen‘𝑏) ∧ 𝑥 ∈ {𝑥}) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
66 | 63, 64, 65 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
67 | | simprrl 804 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑥 ∈ 𝑦) |
68 | 67 | snssd 4340 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ⊆ 𝑦) |
69 | | simprrr 805 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ⊆ {𝑥}) |
70 | 68, 69 | eqssd 3620 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} = 𝑦) |
71 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ∈ 𝑏) |
72 | 70, 71 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ∈ 𝑏) |
73 | 66, 72 | rexlimddv 3035 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝑏) |
74 | 73, 23 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝑏) |
75 | | frn 6053 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝑏 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏) |
76 | 74, 75 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏) |
77 | | ssdomg 8001 |
. . . . . . . . . 10
⊢ (𝑏 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏)) |
78 | 59, 76, 77 | mpsyl 68 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏) |
79 | | simprl 794 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → 𝑏 ≼
ω) |
80 | | domtr 8009 |
. . . . . . . . 9
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏 ∧ 𝑏 ≼ ω) → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
81 | 78, 79, 80 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
82 | 81 | ex 450 |
. . . . . . 7
⊢ ((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) → ((𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
83 | 82 | rexlimdva 3031 |
. . . . . 6
⊢ (𝑋 ∈ V → (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
84 | 58, 83 | syl5bi 232 |
. . . . 5
⊢ (𝑋 ∈ V → (𝒫
𝑋 ∈
2nd𝜔 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
85 | 84 | imp 445 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2nd𝜔)
→ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
86 | 57, 85 | impbida 877 |
. . 3
⊢ (𝑋 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω ↔ 𝒫 𝑋 ∈
2nd𝜔)) |
87 | 18, 86 | bitrd 268 |
. 2
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2nd𝜔)) |
88 | 2, 3, 87 | pm5.21nii 368 |
1
⊢ (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2nd𝜔) |