Definition df-1stc

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

	Ref	Expression
Assertion	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 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1stc	|- 1stc
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6		vy	|- y
7	4	cpw	|- ~P j
8	6	cv	|- y
9		cdom	|- ~<_
10		com	|- _om
11	8 10 9	wbr	|- y ~<_ _om
12		vz	|- z
13	3	cv	|- x
14	12	cv	|- z
15	13 14	wcel	|- x e. z
16	14	cpw	|- ~P z
17	8 16	cin	|- ( y i^i ~P z )
18	17	cuni	|- U. ( y i^i ~P z )
19	13 18	wcel	|- x e. U. ( y i^i ~P z )
20	15 19	wi	|- ( x e. z -> x e. U. ( y i^i ~P z ) )
21	20 12 4	wral	|- A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) )
22	11 21	wa	|- ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) )
23	22 6 7	wrex	|- E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) )
24	23 3 5	wral	|- 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	24 1 2	crab	|- { 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 ) ) ) }
26	0 25	wceq	|- 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 ) ) ) }