df-2ndc

Description: Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010)

		Ref	Expression
	Assertion	df-2ndc	$⊢ 2^{nd} 𝜔 = \{j \| \exists x \in TopBases (x ≼ ω \land topGen (x) = j)\}$

Step	Hyp	Ref	Expression
0		c2ndc	$class 2^{nd} 𝜔$
1		vj	$setvar j$
2		vx	$setvar x$
3		ctb	$class TopBases$
4	2	cv	$setvar x$
5		cdom	$class ≼$
6		com	$class ω$
7	4 6 5	wbr	$wff x ≼ ω$
8		ctg	$class topGen$
9	4 8	cfv	$class topGen (x)$
10	1	cv	$setvar j$
11	9 10	wceq	$wff topGen (x) = j$
12	7 11	wa	$wff (x ≼ ω \land topGen (x) = j)$
13	12 2 3	wrex	$wff \exists x \in TopBases (x ≼ ω \land topGen (x) = j)$
14	13 1	cab	$class \{j \| \exists x \in TopBases (x ≼ ω \land topGen (x) = j)\}$
15	0 14	wceq	$wff 2^{nd} 𝜔 = \{j \| \exists x \in TopBases (x ≼ ω \land topGen (x) = j)\}$

Metamath Proof Explorer