Step | Hyp | Ref
| Expression |
1 | | ctex 8570 |
. 2
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
2 | | pwexr 7506 |
. 2
⊢
(𝒫 𝑋 ∈
2ndω → 𝑋 ∈ V) |
3 | | snex 5298 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
4 | 3 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 → {𝑥} ∈ V)) |
5 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
6 | 5 | sneqr 4726 |
. . . . . . . . 9
⊢ ({𝑥} = {𝑦} → 𝑥 = 𝑦) |
7 | | sneq 4526 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
8 | 6, 7 | impbii 212 |
. . . . . . . 8
⊢ ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦) |
9 | 8 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦))) |
10 | 4, 9 | dom2lem 8595 |
. . . . . 6
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V) |
11 | | f1f1orn 6629 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
13 | | f1oeng 8574 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
14 | 12, 13 | mpdan 687 |
. . . 4
⊢ (𝑋 ∈ V → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
15 | | domen1 8709 |
. . . 4
⊢ (𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) → (𝑋 ≼ ω ↔ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
16 | 14, 15 | syl 17 |
. . 3
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔ ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
17 | | distop 21746 |
. . . . . . 7
⊢ (𝑋 ∈ V → 𝒫 𝑋 ∈ Top) |
18 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
19 | 5 | snelpw 5304 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↔ {𝑥} ∈ 𝒫 𝑋) |
20 | 18, 19 | sylib 221 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
21 | 20 | fmpttd 6889 |
. . . . . . . 8
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋) |
22 | 21 | frnd 6512 |
. . . . . . 7
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋) |
23 | | elpwi 4497 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
24 | 23 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑦 ⊆ 𝑋) |
25 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑦) |
26 | 24, 25 | sseldd 3878 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑋) |
27 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} = {𝑧}) |
28 | | sneq 4526 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
29 | 28 | rspceeqv 3541 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ {𝑧} = {𝑧}) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
30 | 26, 27, 29 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
31 | | snex 5298 |
. . . . . . . . . . 11
⊢ {𝑧} ∈ V |
32 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 ↦ {𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑥}) |
33 | 32 | elrnmpt 5799 |
. . . . . . . . . . 11
⊢ ({𝑧} ∈ V → ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥})) |
34 | 31, 33 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
35 | 30, 34 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
36 | | vsnid 4553 |
. . . . . . . . . 10
⊢ 𝑧 ∈ {𝑧} |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ {𝑧}) |
38 | 25 | snssd 4697 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ⊆ 𝑦) |
39 | | eleq2 2821 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ {𝑧})) |
40 | | sseq1 3902 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑤 ⊆ 𝑦 ↔ {𝑧} ⊆ 𝑦)) |
41 | 39, 40 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑧} → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) ↔ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦))) |
42 | 41 | rspcev 3526 |
. . . . . . . . 9
⊢ (({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∧ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
43 | 35, 37, 38, 42 | syl12anc 836 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
44 | 43 | ralrimivva 3103 |
. . . . . . 7
⊢ (𝑋 ∈ V → ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
45 | | basgen2 21740 |
. . . . . . 7
⊢
((𝒫 𝑋 ∈
Top ∧ ran (𝑥 ∈
𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) → (topGen‘ran (𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
46 | 17, 22, 44, 45 | syl3anc 1372 |
. . . . . 6
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
47 | 46 | adantr 484 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
48 | 46, 17 | eqeltrd 2833 |
. . . . . . 7
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) ∈ Top) |
49 | | tgclb 21721 |
. . . . . . 7
⊢ (ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ↔ (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈ Top) |
50 | 48, 49 | sylibr 237 |
. . . . . 6
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases) |
51 | | 2ndci 22199 |
. . . . . 6
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2ndω) |
52 | 50, 51 | sylan 583 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2ndω) |
53 | 47, 52 | eqeltrrd 2834 |
. . . 4
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → 𝒫 𝑋 ∈
2ndω) |
54 | | is2ndc 22197 |
. . . . . 6
⊢
(𝒫 𝑋 ∈
2ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) |
55 | | vex 3402 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
56 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
57 | 56, 19 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
58 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → (topGen‘𝑏) = 𝒫 𝑋) |
59 | 57, 58 | eleqtrrd 2836 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ (topGen‘𝑏)) |
60 | | vsnid 4553 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ {𝑥} |
61 | | tg2 21716 |
. . . . . . . . . . . . 13
⊢ (({𝑥} ∈ (topGen‘𝑏) ∧ 𝑥 ∈ {𝑥}) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
62 | 59, 60, 61 | sylancl 589 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
63 | | simprrl 781 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑥 ∈ 𝑦) |
64 | 63 | snssd 4697 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ⊆ 𝑦) |
65 | | simprrr 782 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ⊆ {𝑥}) |
66 | 64, 65 | eqssd 3894 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} = 𝑦) |
67 | | simprl 771 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ∈ 𝑏) |
68 | 66, 67 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ∈ 𝑏) |
69 | 62, 68 | rexlimddv 3201 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝑏) |
70 | 69 | fmpttd 6889 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝑏) |
71 | 70 | frnd 6512 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏) |
72 | | ssdomg 8601 |
. . . . . . . . 9
⊢ (𝑏 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏)) |
73 | 55, 71, 72 | mpsyl 68 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏) |
74 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → 𝑏 ≼
ω) |
75 | | domtr 8608 |
. . . . . . . 8
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏 ∧ 𝑏 ≼ ω) → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
76 | 73, 74, 75 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
77 | 76 | rexlimdva2 3197 |
. . . . . 6
⊢ (𝑋 ∈ V → (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
78 | 54, 77 | syl5bi 245 |
. . . . 5
⊢ (𝑋 ∈ V → (𝒫
𝑋 ∈
2ndω → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
79 | 78 | imp 410 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2ndω)
→ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
80 | 53, 79 | impbida 801 |
. . 3
⊢ (𝑋 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω ↔ 𝒫 𝑋 ∈
2ndω)) |
81 | 16, 80 | bitrd 282 |
. 2
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2ndω)) |
82 | 1, 2, 81 | pm5.21nii 383 |
1
⊢ (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2ndω) |