2ndcrest

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

		Ref	Expression
	Assertion	2ndcrest	$⊢ (J \in 2^{nd} 𝜔 \land A \in V) \to J ↾_{𝑡} A \in 2^{nd} 𝜔$

Proof

Step	Hyp	Ref	Expression
1		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J)$
2		simplr	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to x \in TopBases$
3		simpll	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to A \in V$
4		tgrest	$⊢ (x \in TopBases \land A \in V) \to topGen (x ↾_{𝑡} A) = topGen (x) ↾_{𝑡} A$
5	2 3 4	syl2anc	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to topGen (x ↾_{𝑡} A) = topGen (x) ↾_{𝑡} A$
6		restbas	$⊢ x \in TopBases \to x ↾_{𝑡} A \in TopBases$
7	6	ad2antlr	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to x ↾_{𝑡} A \in TopBases$
8		restval	$⊢ (x \in TopBases \land A \in V) \to x ↾_{𝑡} A = ran (y \in x ⟼ y \cap A)$
9	2 3 8	syl2anc	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to x ↾_{𝑡} A = ran (y \in x ⟼ y \cap A)$
10		1stcrestlem	$⊢ x ≼ ω \to ran (y \in x ⟼ y \cap A) ≼ ω$
11	10	adantl	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to ran (y \in x ⟼ y \cap A) ≼ ω$
12	9 11	eqbrtrd	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to (x ↾_{𝑡} A) ≼ ω$
13		2ndci	$⊢ (x ↾_{𝑡} A \in TopBases \land (x ↾_{𝑡} A) ≼ ω) \to topGen (x ↾_{𝑡} A) \in 2^{nd} 𝜔$
14	7 12 13	syl2anc	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to topGen (x ↾_{𝑡} A) \in 2^{nd} 𝜔$
15	5 14	eqeltrrd	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to topGen (x) ↾_{𝑡} A \in 2^{nd} 𝜔$
16		oveq1	$⊢ topGen (x) = J \to topGen (x) ↾_{𝑡} A = J ↾_{𝑡} A$
17	16	eleq1d	$⊢ topGen (x) = J \to (topGen (x) ↾_{𝑡} A \in 2^{nd} 𝜔 \leftrightarrow J ↾_{𝑡} A \in 2^{nd} 𝜔)$
18	15 17	syl5ibcom	$⊢ ((A \in V \land x \in TopBases) \land x ≼ ω) \to (topGen (x) = J \to J ↾_{𝑡} A \in 2^{nd} 𝜔)$
19	18	expimpd	$⊢ (A \in V \land x \in TopBases) \to ((x ≼ ω \land topGen (x) = J) \to J ↾_{𝑡} A \in 2^{nd} 𝜔)$
20	19	rexlimdva	$⊢ A \in V \to (\exists x \in TopBases (x ≼ ω \land topGen (x) = J) \to J ↾_{𝑡} A \in 2^{nd} 𝜔)$
21	1 20	biimtrid	$⊢ A \in V \to (J \in 2^{nd} 𝜔 \to J ↾_{𝑡} A \in 2^{nd} 𝜔)$
22	21	impcom	$⊢ (J \in 2^{nd} 𝜔 \land A \in V) \to J ↾_{𝑡} A \in 2^{nd} 𝜔$

Metamath Proof Explorer

Theorem 2ndcrest

Proof