Metamath Proof Explorer

Theorem 2ndcsb

Description: Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndcsb ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )

Proof

Step Hyp Ref Expression
1 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) )
2 df-rex ⊢ ( ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ↔ ∃ 𝑥 ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) )
3 simprl ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → 𝑥 ≼ ω )
4 ssfii ⊢ ( 𝑥 ∈ TopBases → 𝑥 ⊆ ( fi ‘ 𝑥 ) )
5 fvex ⊢ ( topGen ‘ 𝑥 ) ∈ V
6 bastg ⊢ ( 𝑥 ∈ TopBases → 𝑥 ⊆ ( topGen ‘ 𝑥 ) )
7 6 adantr ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → 𝑥 ⊆ ( topGen ‘ 𝑥 ) )
8 fiss ⊢ ( ( ( topGen ‘ 𝑥 ) ∈ V ∧ 𝑥 ⊆ ( topGen ‘ 𝑥 ) ) → ( fi ‘ 𝑥 ) ⊆ ( fi ‘ ( topGen ‘ 𝑥 ) ) )
9 5 7 8 sylancr ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( fi ‘ 𝑥 ) ⊆ ( fi ‘ ( topGen ‘ 𝑥 ) ) )
10 tgcl ⊢ ( 𝑥 ∈ TopBases → ( topGen ‘ 𝑥 ) ∈ Top )
11 10 adantr ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( topGen ‘ 𝑥 ) ∈ Top )
12 fitop ⊢ ( ( topGen ‘ 𝑥 ) ∈ Top → ( fi ‘ ( topGen ‘ 𝑥 ) ) = ( topGen ‘ 𝑥 ) )
13 11 12 syl ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( fi ‘ ( topGen ‘ 𝑥 ) ) = ( topGen ‘ 𝑥 ) )
14 9 13 sseqtrd ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( fi ‘ 𝑥 ) ⊆ ( topGen ‘ 𝑥 ) )
15 2basgen ⊢ ( ( 𝑥 ⊆ ( fi ‘ 𝑥 ) ∧ ( fi ‘ 𝑥 ) ⊆ ( topGen ‘ 𝑥 ) ) → ( topGen ‘ 𝑥 ) = ( topGen ‘ ( fi ‘ 𝑥 ) ) )
16 4 14 15 syl2an2r ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( topGen ‘ 𝑥 ) = ( topGen ‘ ( fi ‘ 𝑥 ) ) )
17 simprr ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( topGen ‘ 𝑥 ) = 𝐽 )
18 16 17 eqtr3d ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 )
19 3 18 jca ⊢ ( ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )
20 19 eximi ⊢ ( ∃ 𝑥 ( 𝑥 ∈ TopBases ∧ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) ) → ∃ 𝑥 ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )
21 2 20 sylbi ⊢ ( ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → ∃ 𝑥 ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )
22 1 21 sylbi ⊢ ( 𝐽 ∈ 2ndω → ∃ 𝑥 ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )
23 fibas ⊢ ( fi ‘ 𝑥 ) ∈ TopBases
24 simpl ⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) → 𝑥 ≼ ω )
25 fictb ⊢ ( 𝑥 ∈ V → ( 𝑥 ≼ ω ↔ ( fi ‘ 𝑥 ) ≼ ω ) )
26 25 elv ⊢ ( 𝑥 ≼ ω ↔ ( fi ‘ 𝑥 ) ≼ ω )
27 24 26 sylib ⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) → ( fi ‘ 𝑥 ) ≼ ω )
28 simpr ⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) → ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 )
29 27 28 jca ⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) → ( ( fi ‘ 𝑥 ) ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )
30 breq1 ⊢ ( 𝑦 = ( fi ‘ 𝑥 ) → ( 𝑦 ≼ ω ↔ ( fi ‘ 𝑥 ) ≼ ω ) )
31 fveqeq2 ⊢ ( 𝑦 = ( fi ‘ 𝑥 ) → ( ( topGen ‘ 𝑦 ) = 𝐽 ↔ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )
32 30 31 anbi12d ⊢ ( 𝑦 = ( fi ‘ 𝑥 ) → ( ( 𝑦 ≼ ω ∧ ( topGen ‘ 𝑦 ) = 𝐽 ) ↔ ( ( fi ‘ 𝑥 ) ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) ) )
33 32 rspcev ⊢ ( ( ( fi ‘ 𝑥 ) ∈ TopBases ∧ ( ( fi ‘ 𝑥 ) ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) ) → ∃ 𝑦 ∈ TopBases ( 𝑦 ≼ ω ∧ ( topGen ‘ 𝑦 ) = 𝐽 ) )
34 23 29 33 sylancr ⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) → ∃ 𝑦 ∈ TopBases ( 𝑦 ≼ ω ∧ ( topGen ‘ 𝑦 ) = 𝐽 ) )
35 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑦 ∈ TopBases ( 𝑦 ≼ ω ∧ ( topGen ‘ 𝑦 ) = 𝐽 ) )
36 34 35 sylibr ⊢ ( ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) → 𝐽 ∈ 2ndω )
37 36 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) → 𝐽 ∈ 2ndω )
38 22 37 impbii ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ( 𝑥 ≼ ω ∧ ( topGen ‘ ( fi ‘ 𝑥 ) ) = 𝐽 ) )