# 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 ${⊢}\left({J}\in {2}^{nd}𝜔\wedge {A}\in {V}\right)\to {J}{↾}_{𝑡}{A}\in {2}^{nd}𝜔$

### Proof

Step Hyp Ref Expression
1 is2ndc ${⊢}{J}\in {2}^{nd}𝜔↔\exists {x}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({x}\right)={J}\right)$
2 simplr ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to {x}\in \mathrm{TopBases}$
3 simpll ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to {A}\in {V}$
4 tgrest ${⊢}\left({x}\in \mathrm{TopBases}\wedge {A}\in {V}\right)\to \mathrm{topGen}\left({x}{↾}_{𝑡}{A}\right)=\mathrm{topGen}\left({x}\right){↾}_{𝑡}{A}$
5 2 3 4 syl2anc ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{topGen}\left({x}{↾}_{𝑡}{A}\right)=\mathrm{topGen}\left({x}\right){↾}_{𝑡}{A}$
6 restbas ${⊢}{x}\in \mathrm{TopBases}\to {x}{↾}_{𝑡}{A}\in \mathrm{TopBases}$
7 6 ad2antlr ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to {x}{↾}_{𝑡}{A}\in \mathrm{TopBases}$
8 restval ${⊢}\left({x}\in \mathrm{TopBases}\wedge {A}\in {V}\right)\to {x}{↾}_{𝑡}{A}=\mathrm{ran}\left({y}\in {x}⟼{y}\cap {A}\right)$
9 2 3 8 syl2anc ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to {x}{↾}_{𝑡}{A}=\mathrm{ran}\left({y}\in {x}⟼{y}\cap {A}\right)$
10 1stcrestlem ${⊢}{x}\preccurlyeq \mathrm{\omega }\to \mathrm{ran}\left({y}\in {x}⟼{y}\cap {A}\right)\preccurlyeq \mathrm{\omega }$
11 10 adantl ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{ran}\left({y}\in {x}⟼{y}\cap {A}\right)\preccurlyeq \mathrm{\omega }$
12 9 11 eqbrtrd ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to \left({x}{↾}_{𝑡}{A}\right)\preccurlyeq \mathrm{\omega }$
13 2ndci ${⊢}\left({x}{↾}_{𝑡}{A}\in \mathrm{TopBases}\wedge \left({x}{↾}_{𝑡}{A}\right)\preccurlyeq \mathrm{\omega }\right)\to \mathrm{topGen}\left({x}{↾}_{𝑡}{A}\right)\in {2}^{nd}𝜔$
14 7 12 13 syl2anc ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{topGen}\left({x}{↾}_{𝑡}{A}\right)\in {2}^{nd}𝜔$
15 5 14 eqeltrrd ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to \mathrm{topGen}\left({x}\right){↾}_{𝑡}{A}\in {2}^{nd}𝜔$
16 oveq1 ${⊢}\mathrm{topGen}\left({x}\right)={J}\to \mathrm{topGen}\left({x}\right){↾}_{𝑡}{A}={J}{↾}_{𝑡}{A}$
17 16 eleq1d ${⊢}\mathrm{topGen}\left({x}\right)={J}\to \left(\mathrm{topGen}\left({x}\right){↾}_{𝑡}{A}\in {2}^{nd}𝜔↔{J}{↾}_{𝑡}{A}\in {2}^{nd}𝜔\right)$
18 15 17 syl5ibcom ${⊢}\left(\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\wedge {x}\preccurlyeq \mathrm{\omega }\right)\to \left(\mathrm{topGen}\left({x}\right)={J}\to {J}{↾}_{𝑡}{A}\in {2}^{nd}𝜔\right)$
19 18 expimpd ${⊢}\left({A}\in {V}\wedge {x}\in \mathrm{TopBases}\right)\to \left(\left({x}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({x}\right)={J}\right)\to {J}{↾}_{𝑡}{A}\in {2}^{nd}𝜔\right)$
20 19 rexlimdva ${⊢}{A}\in {V}\to \left(\exists {x}\in \mathrm{TopBases}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\wedge \mathrm{topGen}\left({x}\right)={J}\right)\to {J}{↾}_{𝑡}{A}\in {2}^{nd}𝜔\right)$
21 1 20 syl5bi ${⊢}{A}\in {V}\to \left({J}\in {2}^{nd}𝜔\to {J}{↾}_{𝑡}{A}\in {2}^{nd}𝜔\right)$
22 21 impcom ${⊢}\left({J}\in {2}^{nd}𝜔\wedge {A}\in {V}\right)\to {J}{↾}_{𝑡}{A}\in {2}^{nd}𝜔$