Metamath Proof Explorer


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