Metamath Proof Explorer


Theorem restt0

Description: A subspace of a T_0 topology is T_0. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion restt0 ( ( 𝐽 ∈ Kol2 ∧ 𝐴𝑉 ) → ( 𝐽t 𝐴 ) ∈ Kol2 )

Proof

Step Hyp Ref Expression
1 t0top ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )
2 cnt0 ( ( 𝐽 ∈ Kol2 ∧ ( I ↾ ( 𝐴 𝐽 ) ) : ( 𝐴 𝐽 ) –1-1→ ( 𝐴 𝐽 ) ∧ ( I ↾ ( 𝐴 𝐽 ) ) ∈ ( ( 𝐽t 𝐴 ) Cn 𝐽 ) ) → ( 𝐽t 𝐴 ) ∈ Kol2 )
3 1 2 resthauslem ( ( 𝐽 ∈ Kol2 ∧ 𝐴𝑉 ) → ( 𝐽t 𝐴 ) ∈ Kol2 )