Theorem ist1

Description: The predicate "is a T_1 space". (Contributed by FL, 18-Jun-2007)

	Ref	Expression
Hypothesis	ist0.1	|- X = U. J
Assertion	ist1	|- ( J e. Fre <-> ( J e. Top /\ A. a e. X { a } e. ( Clsd ` J ) ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	|- X = U. J
2		unieq	|- ( x = J -> U. x = U. J )
3	2 1	eqtr4di	|- ( x = J -> U. x = X )
4		fveq2	|- ( x = J -> ( Clsd ` x ) = ( Clsd ` J ) )
5	4	eleq2d	|- ( x = J -> ( { a } e. ( Clsd ` x ) <-> { a } e. ( Clsd ` J ) ) )
6	3 5	raleqbidv	|- ( x = J -> ( A. a e. U. x { a } e. ( Clsd ` x ) <-> A. a e. X { a } e. ( Clsd ` J ) ) )
7		df-t1	|- Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }
8	6 7	elrab2	|- ( J e. Fre <-> ( J e. Top /\ A. a e. X { a } e. ( Clsd ` J ) ) )