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 ⊢ J ∈ 2 nd 𝜔 ∧ A ∈ V → J ↾ 𝑡 A ∈ 2 nd 𝜔

Proof

Step Hyp Ref Expression
1 is2ndc ⊢ J ∈ 2 nd 𝜔 ↔ ∃ x ∈ TopBases x ≼ ω ∧ topGen ⁡ x = J
2 simplr ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → x ∈ TopBases
3 simpll ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → A ∈ V
4 tgrest ⊢ x ∈ TopBases ∧ A ∈ V → topGen ⁡ x ↾ 𝑡 A = topGen ⁡ x ↾ 𝑡 A
5 2 3 4 syl2anc ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → topGen ⁡ x ↾ 𝑡 A = topGen ⁡ x ↾ 𝑡 A
6 restbas ⊢ x ∈ TopBases → x ↾ 𝑡 A ∈ TopBases
7 6 ad2antlr ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → x ↾ 𝑡 A ∈ TopBases
8 restval ⊢ x ∈ TopBases ∧ A ∈ V → x ↾ 𝑡 A = ran ⁡ y ∈ x ⟼ y ∩ A
9 2 3 8 syl2anc ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → x ↾ 𝑡 A = ran ⁡ y ∈ x ⟼ y ∩ A
10 1stcrestlem ⊢ x ≼ ω → ran ⁡ y ∈ x ⟼ y ∩ A ≼ ω
11 10 adantl ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → ran ⁡ y ∈ x ⟼ y ∩ A ≼ ω
12 9 11 eqbrtrd ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → x ↾ 𝑡 A ≼ ω
13 2ndci ⊢ x ↾ 𝑡 A ∈ TopBases ∧ x ↾ 𝑡 A ≼ ω → topGen ⁡ x ↾ 𝑡 A ∈ 2 nd 𝜔
14 7 12 13 syl2anc ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → topGen ⁡ x ↾ 𝑡 A ∈ 2 nd 𝜔
15 5 14 eqeltrrd ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → topGen ⁡ x ↾ 𝑡 A ∈ 2 nd 𝜔
16 oveq1 ⊢ topGen ⁡ x = J → topGen ⁡ x ↾ 𝑡 A = J ↾ 𝑡 A
17 16 eleq1d ⊢ topGen ⁡ x = J → topGen ⁡ x ↾ 𝑡 A ∈ 2 nd 𝜔 ↔ J ↾ 𝑡 A ∈ 2 nd 𝜔
18 15 17 syl5ibcom ⊢ A ∈ V ∧ x ∈ TopBases ∧ x ≼ ω → topGen ⁡ x = J → J ↾ 𝑡 A ∈ 2 nd 𝜔
19 18 expimpd ⊢ A ∈ V ∧ x ∈ TopBases → x ≼ ω ∧ topGen ⁡ x = J → J ↾ 𝑡 A ∈ 2 nd 𝜔
20 19 rexlimdva ⊢ A ∈ V → ∃ x ∈ TopBases x ≼ ω ∧ topGen ⁡ x = J → J ↾ 𝑡 A ∈ 2 nd 𝜔
21 1 20 biimtrid ⊢ A ∈ V → J ∈ 2 nd 𝜔 → J ↾ 𝑡 A ∈ 2 nd 𝜔
22 21 impcom ⊢ J ∈ 2 nd 𝜔 ∧ A ∈ V → J ↾ 𝑡 A ∈ 2 nd 𝜔