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