Metamath Proof Explorer


Theorem ist1

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

Ref Expression
Hypothesis ist0.1 𝑋 = 𝐽
Assertion ist1 ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎𝑋 { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 ist0.1 𝑋 = 𝐽
2 unieq ( 𝑥 = 𝐽 𝑥 = 𝐽 )
3 2 1 eqtr4di ( 𝑥 = 𝐽 𝑥 = 𝑋 )
4 fveq2 ( 𝑥 = 𝐽 → ( Clsd ‘ 𝑥 ) = ( Clsd ‘ 𝐽 ) )
5 4 eleq2d ( 𝑥 = 𝐽 → ( { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) ↔ { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )
6 3 5 raleqbidv ( 𝑥 = 𝐽 → ( ∀ 𝑎 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) ↔ ∀ 𝑎𝑋 { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )
7 df-t1 Fre = { 𝑥 ∈ Top ∣ ∀ 𝑎 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }
8 6 7 elrab2 ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎𝑋 { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) )