Theorem restt1

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

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

Proof

Step	Hyp	Ref	Expression
1		t1top	$$⊢J\in \mathrm{Fre}\to J\in \mathrm{Top}$$
2		cnt1	$$⊢\left(J\in \mathrm{Fre}\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{Fre}$$
3	1 2	resthauslem	$$⊢\left(J\in \mathrm{Fre}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}A\in \mathrm{Fre}$$