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

Metamath Proof Explorer

Theorem resthaus

Description: A subspace of a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015) (Proof shortened by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion resthaus ( ( 𝐽 ∈ Haus ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Haus )

Proof

Step Hyp Ref Expression
1 haustop ⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top )
2 cnhaus ⊢ ( ( 𝐽 ∈ Haus ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) : ( 𝐴 ∩ ∪ 𝐽 ) –1-1→ ( 𝐴 ∩ ∪ 𝐽 ) ∧ ( I ↾ ( 𝐴 ∩ ∪ 𝐽 ) ) ∈ ( ( 𝐽 ↾t 𝐴 ) Cn 𝐽 ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Haus )
3 1 2 resthauslem ⊢ ( ( 𝐽 ∈ Haus ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Haus )