is2ndc

Description: The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010) (Revised by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J)$

Step	Hyp	Ref	Expression
1		df-2ndc	$⊢ 2^{nd} 𝜔 = \{j \| \exists x \in TopBases (x ≼ ω \land topGen (x) = j)\}$
2	1	eleq2i	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow J \in \{j \| \exists x \in TopBases (x ≼ ω \land topGen (x) = j)\}$
3		simpr	$⊢ (x ≼ ω \land topGen (x) = J) \to topGen (x) = J$
4		fvex	$⊢ topGen (x) \in V$
5	3 4	eqeltrrdi	$⊢ (x ≼ ω \land topGen (x) = J) \to J \in V$
6	5	rexlimivw	$⊢ \exists x \in TopBases (x ≼ ω \land topGen (x) = J) \to J \in V$
7		eqeq2	$⊢ j = J \to (topGen (x) = j \leftrightarrow topGen (x) = J)$
8	7	anbi2d	$⊢ j = J \to ((x ≼ ω \land topGen (x) = j) \leftrightarrow (x ≼ ω \land topGen (x) = J))$
9	8	rexbidv	$⊢ j = J \to (\exists x \in TopBases (x ≼ ω \land topGen (x) = j) \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J))$
10	6 9	elab3	$⊢ J \in \{j \| \exists x \in TopBases (x ≼ ω \land topGen (x) = j)\} \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J)$
11	2 10	bitri	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists x \in TopBases (x ≼ ω \land topGen (x) = J)$

Metamath Proof Explorer