Definition df-2ndc

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

	Ref	Expression
Assertion	df-2ndc	⊢ 2ndω = { 𝑗 ∣ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2ndc	⊢ 2ndω
1		vj	⊢ 𝑗
2		vx	⊢ 𝑥
3		ctb	⊢ TopBases
4	2	cv	⊢ 𝑥
5		cdom	⊢ ≼
6		com	⊢ ω
7	4 6 5	wbr	⊢ 𝑥 ≼ ω
8		ctg	⊢ topGen
9	4 8	cfv	⊢ ( topGen ‘ 𝑥 )
10	1	cv	⊢ 𝑗
11	9 10	wceq	⊢ ( topGen ‘ 𝑥 ) = 𝑗
12	7 11	wa	⊢ ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 )
13	12 2 3	wrex	⊢ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 )
14	13 1	cab	⊢ { 𝑗 ∣ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) }
15	0 14	wceq	⊢ 2ndω = { 𝑗 ∣ ∃ 𝑥 ∈ TopBases ( 𝑥 ≼ ω ∧ ( topGen ‘ 𝑥 ) = 𝑗 ) }