Theorem 0rest

Description: Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	0rest	$$⊢\varnothing {\upharpoonright }_{𝑡}A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		restval	$$⊢\left(\varnothing \in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \varnothing {\upharpoonright }_{𝑡}A=\mathrm{ran}\left(x\in \varnothing ⟼x\cap A\right)$$
3	1 2	mpan	$$⊢A\in \mathrm{V}\to \varnothing {\upharpoonright }_{𝑡}A=\mathrm{ran}\left(x\in \varnothing ⟼x\cap A\right)$$
4		mpt0	$$⊢\left(x\in \varnothing ⟼x\cap A\right)=\varnothing$$
5	4	rneqi	$$⊢\mathrm{ran}\left(x\in \varnothing ⟼x\cap A\right)=\mathrm{ran}\varnothing$$
6		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
7	5 6	eqtri	$$⊢\mathrm{ran}\left(x\in \varnothing ⟼x\cap A\right)=\varnothing$$
8	3 7	eqtrdi	$$⊢A\in \mathrm{V}\to \varnothing {\upharpoonright }_{𝑡}A=\varnothing$$
9		relxp	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
10		restfn	$$⊢{\upharpoonright }_{𝑡}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
11	10	fndmi	$$⊢\mathrm{dom}{\upharpoonright }_{𝑡}=\mathrm{V}\times \mathrm{V}$$
12	11	releqi	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑡}\leftrightarrow \mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
13	9 12	mpbir	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑡}$$
14	13	ovprc2	$$⊢\neg A\in \mathrm{V}\to \varnothing {\upharpoonright }_{𝑡}A=\varnothing$$
15	8 14	pm2.61i	$$⊢\varnothing {\upharpoonright }_{𝑡}A=\varnothing$$