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

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	$⊢ (J \in Kol2 \land A \in V) \to J ↾_{𝑡} A \in Kol2$

Step	Hyp	Ref	Expression
1		t0top	$⊢ J \in Kol2 \to J \in Top$
2		cnt0	$⊢ (J \in Kol2 \land ({I ↾}_{(A \cap ⋃ J)}) : A \cap ⋃ J \underset{1-1}{⟶} A \cap ⋃ J \land {I ↾}_{(A \cap ⋃ J)} \in ((J ↾_{𝑡} A) Cn J)) \to J ↾_{𝑡} A \in Kol2$
3	1 2	resthauslem	$⊢ (J \in Kol2 \land A \in V) \to J ↾_{𝑡} A \in Kol2$