df-1stc

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

		Ref	Expression
	Assertion	df-1stc	$⊢ 1^{st} 𝜔 = \{j \in Top \| \forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)))\}$

Step	Hyp	Ref	Expression
0		c1stc	$class 1^{st} 𝜔$
1		vj	$setvar j$
2		ctop	$class Top$
3		vx	$setvar x$
4	1	cv	$setvar j$
5	4	cuni	$class ⋃ j$
6		vy	$setvar y$
7	4	cpw	$class 𝒫 j$
8	6	cv	$setvar y$
9		cdom	$class ≼$
10		com	$class ω$
11	8 10 9	wbr	$wff y ≼ ω$
12		vz	$setvar z$
13	3	cv	$setvar x$
14	12	cv	$setvar z$
15	13 14	wcel	$wff x \in z$
16	14	cpw	$class 𝒫 z$
17	8 16	cin	$class (y \cap 𝒫 z)$
18	17	cuni	$class ⋃ (y \cap 𝒫 z)$
19	13 18	wcel	$wff x \in ⋃ (y \cap 𝒫 z)$
20	15 19	wi	$wff (x \in z \to x \in ⋃ (y \cap 𝒫 z))$
21	20 12 4	wral	$wff \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z))$
22	11 21	wa	$wff (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)))$
23	22 6 7	wrex	$wff \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)))$
24	23 3 5	wral	$wff \forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)))$
25	24 1 2	crab	$class \{j \in Top \| \forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)))\}$
26	0 25	wceq	$wff 1^{st} 𝜔 = \{j \in Top \| \forall x \in ⋃ j \exists y \in 𝒫 j (y ≼ ω \land \forall z \in j (x \in z \to x \in ⋃ (y \cap 𝒫 z)))\}$

Metamath Proof Explorer