Definition df-2ndc 21053

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

Assertion

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

Distinct variable group:   𝑥,𝑗

Detailed syntax breakdown of Definition df-2ndc

Step	Hyp	Ref	Expression
1		c2ndc 21051	. 2 class 2nd𝜔
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1474	. . . . . 6 class 𝑥
4		com 6957	. . . . . 6 class ω
5		cdom 7839	. . . . . 6 class ≼
6	3, 4, 5	wbr 4583	. . . . 5 wff 𝑥 ≼ ω
7		ctg 15921	. . . . . . 7 class topGen
8	3, 7	cfv 5804	. . . . . 6 class (topGen‘𝑥)
9		vj	. . . . . . 7 setvar 𝑗
10	9	cv 1474	. . . . . 6 class 𝑗
11	8, 10	wceq 1475	. . . . 5 wff (topGen‘𝑥) = 𝑗
12	6, 11	wa 383	. . . 4 wff (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
13		ctb 20520	. . . 4 class TopBases
14	12, 2, 13	wrex 2897	. . 3 wff ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
15	14, 9	cab 2596	. 2 class {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
16	1, 15	wceq 1475	1 wff 2nd𝜔 = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}

This definition is referenced by:  is2ndc  21059