Definition df-1stc 22498

Description: Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)

Assertion

Ref	Expression
df-1stc	⊢ 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}

Distinct variable group:   𝑥,𝑗,𝑦,𝑧

Detailed syntax breakdown of Definition df-1stc

Step	Hyp	Ref	Expression
1		c1stc 22496	. 2 class 1stω
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1538	. . . . . . 7 class 𝑦
4		com 7687	. . . . . . 7 class ω
5		cdom 8689	. . . . . . 7 class ≼
6	3, 4, 5	wbr 5070	. . . . . 6 wff 𝑦 ≼ ω
7		vx	. . . . . . . . 9 setvar 𝑥
8		vz	. . . . . . . . 9 setvar 𝑧
9	7, 8	wel 2109	. . . . . . . 8 wff 𝑥 ∈ 𝑧
10	7	cv 1538	. . . . . . . . 9 class 𝑥
11	8	cv 1538	. . . . . . . . . . . 12 class 𝑧
12	11	cpw 4530	. . . . . . . . . . 11 class 𝒫 𝑧
13	3, 12	cin 3882	. . . . . . . . . 10 class (𝑦 ∩ 𝒫 𝑧)
14	13	cuni 4836	. . . . . . . . 9 class ∪ (𝑦 ∩ 𝒫 𝑧)
15	10, 14	wcel 2108	. . . . . . . 8 wff 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)
16	9, 15	wi 4	. . . . . . 7 wff (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))
17		vj	. . . . . . . 8 setvar 𝑗
18	17	cv 1538	. . . . . . 7 class 𝑗
19	16, 8, 18	wral 3063	. . . . . 6 wff ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))
20	6, 19	wa 395	. . . . 5 wff (𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
21	18	cpw 4530	. . . . 5 class 𝒫 𝑗
22	20, 2, 21	wrex 3064	. . . 4 wff ∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
23	18	cuni 4836	. . . 4 class ∪ 𝑗
24	22, 7, 23	wral 3063	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
25		ctop 21950	. . 3 class Top
26	24, 17, 25	crab 3067	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}
27	1, 26	wceq 1539	1 wff 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}

This definition is referenced by:  is1stc  22500