Metamath Proof Explorer

Theorem dis2ndc

Description: A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Assertion dis2ndc ( 𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω )

Proof

Step Hyp Ref Expression
1 ctex ⊢ ( 𝑋 ≼ ω → 𝑋 ∈ V )
2 pwexr ⊢ ( 𝒫 𝑋 ∈ 2ndω → 𝑋 ∈ V )
3 vsnex ⊢ { 𝑥 } ∈ V
4 3 2a1i ⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 → { 𝑥 } ∈ V ) )
5 vex ⊢ 𝑥 ∈ V
6 5 sneqr ⊢ ( { 𝑥 } = { 𝑦 } → 𝑥 = 𝑦 )
7 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
8 6 7 impbii ⊢ ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 )
9 8 2a1i ⊢ ( 𝑋 ∈ V → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) ) )
10 4 9 dom2lem ⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 –1-1→ V )
11 f1f1orn ⊢ ( ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 –1-1→ V → ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 –1-1-onto→ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) )
12 10 11 syl ⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 –1-1-onto→ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) )
13 f1oeng ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 –1-1-onto→ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) → 𝑋 ≈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) )
14 12 13 mpdan ⊢ ( 𝑋 ∈ V → 𝑋 ≈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) )
15 domen1 ⊢ ( 𝑋 ≈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) → ( 𝑋 ≼ ω ↔ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) )
16 14 15 syl ⊢ ( 𝑋 ∈ V → ( 𝑋 ≼ ω ↔ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) )
17 distop ⊢ ( 𝑋 ∈ V → 𝒫 𝑋 ∈ Top )
18 5 snelpw ⊢ ( 𝑥 ∈ 𝑋 ↔ { 𝑥 } ∈ 𝒫 𝑋 )
19 18 bilani ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝒫 𝑋 )
20 19 fmpttd ⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 ⟶ 𝒫 𝑋 )
21 20 frnd ⊢ ( 𝑋 ∈ V → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝒫 𝑋 )
22 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
23 22 ad2antrl ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑦 ⊆ 𝑋 )
24 simprr ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ 𝑦 )
25 23 24 sseldd ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ 𝑋 )
26 eqidd ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → { 𝑧 } = { 𝑧 } )
27 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
28 27 rspceeqv ⊢ ( ( 𝑧 ∈ 𝑋 ∧ { 𝑧 } = { 𝑧 } ) → ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } )
29 25 26 28 syl2anc ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } )
30 vsnex ⊢ { 𝑧 } ∈ V
31 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } )
32 31 elrnmpt ⊢ ( { 𝑧 } ∈ V → ( { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } ) )
33 30 32 ax-mp ⊢ ( { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } )
34 29 33 sylibr ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) )
35 vsnid ⊢ 𝑧 ∈ { 𝑧 }
36 35 a1i ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ { 𝑧 } )
37 24 snssd ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → { 𝑧 } ⊆ 𝑦 )
38 eleq2 ⊢ ( 𝑤 = { 𝑧 } → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ { 𝑧 } ) )
39 sseq1 ⊢ ( 𝑤 = { 𝑧 } → ( 𝑤 ⊆ 𝑦 ↔ { 𝑧 } ⊆ 𝑦 ) )
40 38 39 anbi12d ⊢ ( 𝑤 = { 𝑧 } → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ↔ ( 𝑧 ∈ { 𝑧 } ∧ { 𝑧 } ⊆ 𝑦 ) ) )
41 40 rspcev ⊢ ( ( { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∧ ( 𝑧 ∈ { 𝑧 } ∧ { 𝑧 } ⊆ 𝑦 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) )
42 34 36 37 41 syl12anc ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) )
43 42 ralrimivva ⊢ ( 𝑋 ∈ V → ∀ 𝑦 ∈ 𝒫 𝑋 ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) )
44 basgen2 ⊢ ( ( 𝒫 𝑋 ∈ Top ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) = 𝒫 𝑋 )
45 17 21 43 44 syl3anc ⊢ ( 𝑋 ∈ V → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) = 𝒫 𝑋 )
46 45 adantr ⊢ ( ( 𝑋 ∈ V ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) = 𝒫 𝑋 )
47 45 17 eqeltrd ⊢ ( 𝑋 ∈ V → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ Top )
48 tgclb ⊢ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∈ TopBases ↔ ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ Top )
49 47 48 sylibr ⊢ ( 𝑋 ∈ V → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∈ TopBases )
50 2ndci ⊢ ( ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∈ TopBases ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ 2ndω )
51 49 50 sylan ⊢ ( ( 𝑋 ∈ V ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ 2ndω )
52 46 51 eqeltrrd ⊢ ( ( 𝑋 ∈ V ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → 𝒫 𝑋 ∈ 2ndω )
53 is2ndc ⊢ ( 𝒫 𝑋 ∈ 2ndω ↔ ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) )
54 vex ⊢ 𝑏 ∈ V
55 18 bilani ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝒫 𝑋 )
56 simplrr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( topGen ‘ 𝑏 ) = 𝒫 𝑋 )
57 55 56 eleqtrrd ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ ( topGen ‘ 𝑏 ) )
58 vsnid ⊢ 𝑥 ∈ { 𝑥 }
59 tg2 ⊢ ( ( { 𝑥 } ∈ ( topGen ‘ 𝑏 ) ∧ 𝑥 ∈ { 𝑥 } ) → ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) )
60 57 58 59 sylancl ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) )
61 simprrl ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → 𝑥 ∈ 𝑦 )
62 61 snssd ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → { 𝑥 } ⊆ 𝑦 )
63 simprrr ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → 𝑦 ⊆ { 𝑥 } )
64 62 63 eqssd ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → { 𝑥 } = 𝑦 )
65 simprl ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → 𝑦 ∈ 𝑏 )
66 64 65 eqeltrd ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → { 𝑥 } ∈ 𝑏 )
67 60 66 rexlimddv ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝑏 )
68 67 fmpttd ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 ⟶ 𝑏 )
69 68 frnd ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝑏 )
70 ssdomg ⊢ ( 𝑏 ∈ V → ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝑏 → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ 𝑏 ) )
71 54 69 70 mpsyl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ 𝑏 )
72 simprl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → 𝑏 ≼ ω )
73 domtr ⊢ ( ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ 𝑏 ∧ 𝑏 ≼ ω ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω )
74 71 72 73 syl2anc ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω )
75 74 rexlimdva2 ⊢ ( 𝑋 ∈ V → ( ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) )
76 53 75 biimtrid ⊢ ( 𝑋 ∈ V → ( 𝒫 𝑋 ∈ 2ndω → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) )
77 76 imp ⊢ ( ( 𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2ndω ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω )
78 52 77 impbida ⊢ ( 𝑋 ∈ V → ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω ) )
79 16 78 bitrd ⊢ ( 𝑋 ∈ V → ( 𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω ) )
80 1 2 79 pm5.21nii ⊢ ( 𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω )