This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) }