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	|- 1stc = { j e. Top | A. x e. U. j E. y e. ~P j ( y ~<_ om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) }

Distinct variable group:   x, j, y, z

Detailed syntax breakdown of Definition df-1stc

Step	Hyp	Ref	Expression
1		c1stc 21240	. 2 class 1stc
2		vy	. . . . . . . 8 setvar y
3	2	cv 1482	. . . . . . 7 class y
4		com 7065	. . . . . . 7 class om
5		cdom 7953	. . . . . . 7 class ~<_
6	3, 4, 5	wbr 4653	. . . . . 6 wff y ~<_ om
7		vx	. . . . . . . . 9 setvar x
8		vz	. . . . . . . . 9 setvar z
9	7, 8	wel 1991	. . . . . . . 8 wff x e. z
10	7	cv 1482	. . . . . . . . 9 class x
11	8	cv 1482	. . . . . . . . . . . 12 class z
12	11	cpw 4158	. . . . . . . . . . 11 class ~P z
13	3, 12	cin 3573	. . . . . . . . . 10 class ( y i^i ~P z )
14	13	cuni 4436	. . . . . . . . 9 class U. ( y i^i ~P z )
15	10, 14	wcel 1990	. . . . . . . 8 wff x e. U. ( y i^i ~P z )
16	9, 15	wi 4	. . . . . . 7 wff ( x e. z -> x e. U. ( y i^i ~P z ) )
17		vj	. . . . . . . 8 setvar j
18	17	cv 1482	. . . . . . 7 class j
19	16, 8, 18	wral 2912	. . . . . 6 wff A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) )
20	6, 19	wa 384	. . . . 5 wff ( y ~<_ om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) )
21	18	cpw 4158	. . . . 5 class ~P j
22	20, 2, 21	wrex 2913	. . . 4 wff E. y e. ~P j ( y ~<_ om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) )
23	18	cuni 4436	. . . 4 class U. j
24	22, 7, 23	wral 2912	. . 3 wff A. x e. U. j E. y e. ~P j ( y ~<_ om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) )
25		ctop 20698	. . 3 class Top
26	24, 17, 25	crab 2916	. 2 class { j e. Top | A. x e. U. j E. y e. ~P j ( y ~<_ om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) }
27	1, 26	wceq 1483	1 wff 1stc = { j e. Top | A. x e. U. j E. y e. ~P j ( y ~<_ om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) }

This definition is referenced by:  is1stc  21244