Metamath Proof Explorer

Theorem 2ndcrest

Description: A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 2ndcrest ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ 2ndω )

Proof

Step Hyp Ref Expression
1 is2ndc ⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) )
2 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → 𝑥 ∈ TopBases )
3 simpll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → 𝐴 ∈ 𝑉 )
4 tgrest ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝐴 ∈ 𝑉 ) → ( topGen ‘ ( 𝑥 ↾t 𝐴 ) ) = ( ( topGen ‘ 𝑥 ) ↾t 𝐴 ) )
5 2 3 4 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ( topGen ‘ ( 𝑥 ↾t 𝐴 ) ) = ( ( topGen ‘ 𝑥 ) ↾t 𝐴 ) )
6 restbas ⊢ ( 𝑥 ∈ TopBases → ( 𝑥 ↾t 𝐴 ) ∈ TopBases )
7 6 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ( 𝑥 ↾t 𝐴 ) ∈ TopBases )
8 restval ⊢ ( ( 𝑥 ∈ TopBases ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ↾t 𝐴 ) = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ 𝐴 ) ) )
9 2 3 8 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ( 𝑥 ↾t 𝐴 ) = ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ 𝐴 ) ) )
10 1stcrestlem ⊢ ( 𝑥 ≼ ω → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ 𝐴 ) ) ≼ ω )
11 10 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ 𝐴 ) ) ≼ ω )
12 9 11 eqbrtrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ( 𝑥 ↾t 𝐴 ) ≼ ω )
13 2ndci ⊢ ( ( ( 𝑥 ↾t 𝐴 ) ∈ TopBases ∧ ( 𝑥 ↾t 𝐴 ) ≼ ω ) → ( topGen ‘ ( 𝑥 ↾t 𝐴 ) ) ∈ 2ndω )
14 7 12 13 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ( topGen ‘ ( 𝑥 ↾t 𝐴 ) ) ∈ 2ndω )
15 5 14 eqeltrrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ( ( topGen ‘ 𝑥 ) ↾t 𝐴 ) ∈ 2ndω )
16 oveq1 ⊢ ( ( topGen ‘ 𝑥 ) = 𝐽 → ( ( topGen ‘ 𝑥 ) ↾t 𝐴 ) = ( 𝐽 ↾t 𝐴 ) )
17 16 eleq1d ⊢ ( ( topGen ‘ 𝑥 ) = 𝐽 → ( ( ( topGen ‘ 𝑥 ) ↾t 𝐴 ) ∈ 2ndω ↔ ( 𝐽 ↾t 𝐴 ) ∈ 2ndω ) )
18 15 17 syl5ibcom ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) ∧ 𝑥 ≼ ω ) → ( ( topGen ‘ 𝑥 ) = 𝐽 → ( 𝐽 ↾t 𝐴 ) ∈ 2ndω ) )
19 18 expimpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ TopBases ) → ( ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → ( 𝐽 ↾t 𝐴 ) ∈ 2ndω ) )
20 19 rexlimdva ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝐽 ) → ( 𝐽 ↾t 𝐴 ) ∈ 2ndω ) )
21 1 20 syl5bi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐽 ∈ 2ndω → ( 𝐽 ↾t 𝐴 ) ∈ 2ndω ) )
22 21 impcom ⊢ ( ( 𝐽 ∈ 2ndω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ 2ndω )