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 snex ⊢ { 𝑥 } ∈ 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 simpr ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
19 5 snelpw ⊢ ( 𝑥 ∈ 𝑋 ↔ { 𝑥 } ∈ 𝒫 𝑋 )
20 18 19 sylib ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝒫 𝑋 )
21 20 fmpttd ⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 ⟶ 𝒫 𝑋 )
22 21 frnd ⊢ ( 𝑋 ∈ V → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝒫 𝑋 )
23 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋 )
24 23 ad2antrl ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑦 ⊆ 𝑋 )
25 simprr ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ 𝑦 )
26 24 25 sseldd ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ 𝑋 )
27 eqidd ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → { 𝑧 } = { 𝑧 } )
28 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
29 28 rspceeqv ⊢ ( ( 𝑧 ∈ 𝑋 ∧ { 𝑧 } = { 𝑧 } ) → ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } )
30 26 27 29 syl2anc ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } )
31 snex ⊢ { 𝑧 } ∈ V
32 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } )
33 32 elrnmpt ⊢ ( { 𝑧 } ∈ V → ( { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } ) )
34 31 33 ax-mp ⊢ ( { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑧 } = { 𝑥 } )
35 30 34 sylibr ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) )
36 vsnid ⊢ 𝑧 ∈ { 𝑧 }
37 36 a1i ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → 𝑧 ∈ { 𝑧 } )
38 25 snssd ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → { 𝑧 } ⊆ 𝑦 )
39 eleq2 ⊢ ( 𝑤 = { 𝑧 } → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ { 𝑧 } ) )
40 sseq1 ⊢ ( 𝑤 = { 𝑧 } → ( 𝑤 ⊆ 𝑦 ↔ { 𝑧 } ⊆ 𝑦 ) )
41 39 40 anbi12d ⊢ ( 𝑤 = { 𝑧 } → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ↔ ( 𝑧 ∈ { 𝑧 } ∧ { 𝑧 } ⊆ 𝑦 ) ) )
42 41 rspcev ⊢ ( ( { 𝑧 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∧ ( 𝑧 ∈ { 𝑧 } ∧ { 𝑧 } ⊆ 𝑦 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) )
43 35 37 38 42 syl12anc ⊢ ( ( 𝑋 ∈ V ∧ ( 𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦 ) ) → ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) )
44 43 ralrimivva ⊢ ( 𝑋 ∈ V → ∀ 𝑦 ∈ 𝒫 𝑋 ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) )
45 basgen2 ⊢ ( ( 𝒫 𝑋 ∈ Top ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝒫 𝑋 ∧ ∀ 𝑦 ∈ 𝒫 𝑋 ∀ 𝑧 ∈ 𝑦 ∃ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) = 𝒫 𝑋 )
46 17 22 44 45 syl3anc ⊢ ( 𝑋 ∈ V → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) = 𝒫 𝑋 )
47 46 adantr ⊢ ( ( 𝑋 ∈ V ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) = 𝒫 𝑋 )
48 46 17 eqeltrd ⊢ ( 𝑋 ∈ V → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ Top )
49 tgclb ⊢ ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∈ TopBases ↔ ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ Top )
50 48 49 sylibr ⊢ ( 𝑋 ∈ V → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∈ TopBases )
51 2ndci ⊢ ( ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ∈ TopBases ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ 2ndω )
52 50 51 sylan ⊢ ( ( 𝑋 ∈ V ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → ( topGen ‘ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ) ∈ 2ndω )
53 47 52 eqeltrrd ⊢ ( ( 𝑋 ∈ V ∧ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) → 𝒫 𝑋 ∈ 2ndω )
54 is2ndc ⊢ ( 𝒫 𝑋 ∈ 2ndω ↔ ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) )
55 vex ⊢ 𝑏 ∈ V
56 simpr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
57 56 19 sylib ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝒫 𝑋 )
58 simplrr ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( topGen ‘ 𝑏 ) = 𝒫 𝑋 )
59 57 58 eleqtrrd ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ ( topGen ‘ 𝑏 ) )
60 vsnid ⊢ 𝑥 ∈ { 𝑥 }
61 tg2 ⊢ ( ( { 𝑥 } ∈ ( topGen ‘ 𝑏 ) ∧ 𝑥 ∈ { 𝑥 } ) → ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) )
62 59 60 61 sylancl ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑏 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) )
63 simprrl ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → 𝑥 ∈ 𝑦 )
64 63 snssd ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → { 𝑥 } ⊆ 𝑦 )
65 simprrr ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → 𝑦 ⊆ { 𝑥 } )
66 64 65 eqssd ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → { 𝑥 } = 𝑦 )
67 simprl ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → 𝑦 ∈ 𝑏 )
68 66 67 eqeltrd ⊢ ( ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑏 ∧ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ { 𝑥 } ) ) ) → { 𝑥 } ∈ 𝑏 )
69 62 68 rexlimddv ⊢ ( ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ 𝑏 )
70 69 fmpttd ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) : 𝑋 ⟶ 𝑏 )
71 70 frnd ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝑏 )
72 ssdomg ⊢ ( 𝑏 ∈ V → ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ⊆ 𝑏 → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ 𝑏 ) )
73 55 71 72 mpsyl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ 𝑏 )
74 simprl ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → 𝑏 ≼ ω )
75 domtr ⊢ ( ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ 𝑏 ∧ 𝑏 ≼ ω ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω )
76 73 74 75 syl2anc ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑏 ∈ TopBases ) ∧ ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω )
77 76 rexlimdva2 ⊢ ( 𝑋 ∈ V → ( ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ ( topGen ‘ 𝑏 ) = 𝒫 𝑋 ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) )
78 54 77 syl5bi ⊢ ( 𝑋 ∈ V → ( 𝒫 𝑋 ∈ 2ndω → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ) )
79 78 imp ⊢ ( ( 𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2ndω ) → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω )
80 53 79 impbida ⊢ ( 𝑋 ∈ V → ( ran ( 𝑥 ∈ 𝑋 ↦ { 𝑥 } ) ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω ) )
81 16 80 bitrd ⊢ ( 𝑋 ∈ V → ( 𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω ) )
82 1 2 81 pm5.21nii ⊢ ( 𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω )