Description: The predicate "is a T_1 space". (Contributed by FL, 18-Jun-2007)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ist0.1 | ⊢ 𝑋 = ∪ 𝐽 | |
Assertion | ist1 | ⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎 ∈ 𝑋 { 𝑎 } ∈ ( Clsd ‘ 𝐽 ) ) ) |
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 ‘ 𝐽 ) ) ) |