Theorem restt0

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

	Ref	Expression
Assertion	restt0	$$⊢\left(J\in \mathrm{Kol2}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}A\in \mathrm{Kol2}$$

Proof

Step	Hyp	Ref	Expression
1		t0top	$$⊢J\in \mathrm{Kol2}\to J\in \mathrm{Top}$$
2		cnt0	$$⊢\left(J\in \mathrm{Kol2}\wedge \left({\mathrm{I}\upharpoonright }_{\left(A\cap \bigcup J\right)}\right):A\cap \bigcup J\underset{1-1}{⟶}A\cap \bigcup J\wedge {\mathrm{I}\upharpoonright }_{\left(A\cap \bigcup J\right)}\in \left(\left(J{\upharpoonright }_{𝑡}A\right)\mathrm{Cn}J\right)\right)\to J{\upharpoonright }_{𝑡}A\in \mathrm{Kol2}$$
3	1 2	resthauslem	$$⊢\left(J\in \mathrm{Kol2}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}A\in \mathrm{Kol2}$$