Definition df-1stc 21242

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 21240	. 2 class 1st𝜔
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1482	. . . . . . 7 class 𝑦
4		com 7065	. . . . . . 7 class ω
5		cdom 7953	. . . . . . 7 class ≼
6	3, 4, 5	wbr 4653	. . . . . 6 wff 𝑦 ≼ ω
7		vx	. . . . . . . . 9 setvar 𝑥
8		vz	. . . . . . . . 9 setvar 𝑧
9	7, 8	wel 1991	. . . . . . . 8 wff 𝑥 ∈ 𝑧
10	7	cv 1482	. . . . . . . . 9 class 𝑥
11	8	cv 1482	. . . . . . . . . . . 12 class 𝑧
12	11	cpw 4158	. . . . . . . . . . 11 class 𝒫 𝑧
13	3, 12	cin 3573	. . . . . . . . . 10 class (𝑦 ∩ 𝒫 𝑧)
14	13	cuni 4436	. . . . . . . . 9 class ∪ (𝑦 ∩ 𝒫 𝑧)
15	10, 14	wcel 1990	. . . . . . . 8 wff 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)
16	9, 15	wi 4	. . . . . . 7 wff (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))
17		vj	. . . . . . . 8 setvar 𝑗
18	17	cv 1482	. . . . . . 7 class 𝑗
19	16, 8, 18	wral 2912	. . . . . 6 wff ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))
20	6, 19	wa 384	. . . . 5 wff (𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
21	18	cpw 4158	. . . . 5 class 𝒫 𝑗
22	20, 2, 21	wrex 2913	. . . 4 wff ∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
23	18	cuni 4436	. . . 4 class ∪ 𝑗
24	22, 7, 23	wral 2912	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))
25		ctop 20698	. . 3 class Top
26	24, 17, 25	crab 2916	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}
27	1, 26	wceq 1483	1 wff 1st𝜔 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}

This definition is referenced by:  is1stc  21244