Theorem restrcl

Description: Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 1-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		0opn	$$⊢J{\upharpoonright }_{𝑡}A\in \mathrm{Top}\to \varnothing \in \left(J{\upharpoonright }_{𝑡}A\right)$$
2		n0i	$$⊢\varnothing \in \left(J{\upharpoonright }_{𝑡}A\right)\to \neg J{\upharpoonright }_{𝑡}A=\varnothing$$
3	1 2	syl	$$⊢J{\upharpoonright }_{𝑡}A\in \mathrm{Top}\to \neg J{\upharpoonright }_{𝑡}A=\varnothing$$
4		restfn	$$⊢{\upharpoonright }_{𝑡}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
5	4	fndmi	$$⊢\mathrm{dom}{\upharpoonright }_{𝑡}=\mathrm{V}\times \mathrm{V}$$
6	5	ndmov	$$⊢\neg \left(J\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to J{\upharpoonright }_{𝑡}A=\varnothing$$
7	3 6	nsyl2	$$⊢J{\upharpoonright }_{𝑡}A\in \mathrm{Top}\to \left(J\in \mathrm{V}\wedge A\in \mathrm{V}\right)$$