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

Metamath Proof Explorer

Theorem is1stc

Description: The predicate "is a first-countable topology." This can be described as "every point has a countable local basis" - that is, every point has a countable collection of open sets containing it such that every open set containing the point has an open set from this collection as a subset. (Contributed by Jeff Hankins, 22-Aug-2009)

Ref Expression
Hypothesis is1stc.1 
|- X = U. J
Assertion is1stc 
|- ( J e. 1stc <-> ( J e. Top /\ A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 is1stc.1 
 |-  X = U. J
2 unieq 
 |-  ( j = J -> U. j = U. J )
3 2 1 eqtr4di 
 |-  ( j = J -> U. j = X )
4 pweq 
 |-  ( j = J -> ~P j = ~P J )
5 raleq 
 |-  ( j = J -> ( A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) <-> A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) )
6 5 anbi2d 
 |-  ( j = J -> ( ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) <-> ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) )
7 4 6 rexeqbidv 
 |-  ( j = J -> ( E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> x e. U. ( y i^i ~P z ) ) ) <-> E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) )
8 3 7 raleqbidv 
 |-  ( j = J -> ( 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 ) ) ) <-> A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) )
9 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 ) ) ) }
10 8 9 elrab2 
 |-  ( J e. 1stc <-> ( J e. Top /\ A. x e. X E. y e. ~P J ( y ~<_ _om /\ A. z e. J ( x e. z -> x e. U. ( y i^i ~P z ) ) ) ) )