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

Metamath Proof Explorer

Definition df-t1

Description: The class of all T_1 spaces, also called Fréchet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007)

Ref Expression
Assertion df-t1 Fre = { 𝑥 ∈ Top ∣ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ct1 ⊢ Fre
1 vx ⊢ 𝑥
2 ctop ⊢ Top
3 va ⊢ 𝑎
4 1 cv ⊢ 𝑥
5 4 cuni ⊢ ∪ 𝑥
6 3 cv ⊢ 𝑎
7 6 csn ⊢ { 𝑎 }
8 ccld ⊢ Clsd
9 4 8 cfv ⊢ ( Clsd ‘ 𝑥 )
10 7 9 wcel ⊢ { 𝑎 } ∈ ( Clsd ‘ 𝑥 )
11 10 3 5 wral ⊢ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 )
12 11 1 2 crab ⊢ { 𝑥 ∈ Top ∣ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }
13 0 12 wceq ⊢ Fre = { 𝑥 ∈ Top ∣ ∀ 𝑎 ∈ ∪ 𝑥 { 𝑎 } ∈ ( Clsd ‘ 𝑥 ) }