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

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 = ⋃ J
Assertion ist1 ⊢ J ∈ Fre ↔ J ∈ Top ∧ ∀ a ∈ X a ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 ist0.1 ⊢ X = ⋃ J
2 unieq ⊢ x = J → ⋃ x = ⋃ J
3 2 1 eqtr4di ⊢ x = J → ⋃ x = X
4 fveq2 ⊢ x = J → Clsd ⁡ x = Clsd ⁡ J
5 4 eleq2d ⊢ x = J → a ∈ Clsd ⁡ x ↔ a ∈ Clsd ⁡ J
6 3 5 raleqbidv ⊢ x = J → ∀ a ∈ ⋃ x a ∈ Clsd ⁡ x ↔ ∀ a ∈ X a ∈ Clsd ⁡ J
7 df-t1 ⊢ Fre = x ∈ Top | ∀ a ∈ ⋃ x a ∈ Clsd ⁡ x
8 6 7 elrab2 ⊢ J ∈ Fre ↔ J ∈ Top ∧ ∀ a ∈ X a ∈ Clsd ⁡ J