Definition df-1stc 23757

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 23755	. 2 class 1stω
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1569	. . . . . . 7 class 𝑦
4		com 7877	. . . . . . 7 class ω
5		cdom 8971	. . . . . . 7 class ≼
6	3, 4, 5	wbr 5103	. . . . . 6 wff 𝑦 ≼ ω
7		vx	. . . . . . . . 9 setvar 𝑥
8		vz	. . . . . . . . 9 setvar 𝑧
9	7, 8	wel 2146	. . . . . . . 8 wff 𝑥 ∈ 𝑧
10	7	cv 1569	. . . . . . . . 9 class 𝑥
11	8	cv 1569	. . . . . . . . . . . 12 class 𝑧
12	11	cpw 4557	. . . . . . . . . . 11 class 𝒫 𝑧
13	3, 12	cin 3898	. . . . . . . . . 10 class (𝑦 ∩ 𝒫 𝑧)
14	13	cuni 4867	. . . . . . . . 9 class ∪ (𝑦 ∩ 𝒫 𝑧)
15	10, 14	wcel 2145	. . . . . . . 8 wff 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)
16	9, 15	wi 4	. . . . . . 7 wff (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))
17		vj	. . . . . . . 8 setvar 𝑗
18	17	cv 1569	. . . . . . 7 class 𝑗
19	16, 8, 18	wral 3077	. . . . . 6 wff ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))
20	6, 19	wa 401	. . . . 5 wff (𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
21	18	cpw 4557	. . . . 5 class 𝒫 𝑗
22	20, 2, 21	wrex 3087	. . . 4 wff ∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
23	18	cuni 4867	. . . 4 class ∪ 𝑗
24	22, 7, 23	wral 3077	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
25		ctop 23211	. . 3 class Top
26	24, 17, 25	crab 3413	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}
27	1, 26	wceq 1570	1 wff 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}

This definition is used by:  is1stc  23759