Theorem restin

Description: When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013)

	Ref	Expression
Hypothesis	restin.1	$$⊢X=\bigcup J$$
Assertion	restin	$$⊢\left(J\in V\wedge A\in W\right)\to J{\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}\left(A\cap X\right)$$

Proof

Step	Hyp	Ref	Expression
1		restin.1	$$⊢X=\bigcup J$$
2		uniexg	$$⊢J\in V\to \bigcup J\in \mathrm{V}$$
3	1 2	eqeltrid	$$⊢J\in V\to X\in \mathrm{V}$$
4	3	adantr	$$⊢\left(J\in V\wedge A\in W\right)\to X\in \mathrm{V}$$
5		restco	$$⊢\left(J\in V\wedge X\in \mathrm{V}\wedge A\in W\right)\to \left(J{\upharpoonright }_{𝑡}X\right){\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}\left(X\cap A\right)$$
6	5	3com23	$$⊢\left(J\in V\wedge A\in W\wedge X\in \mathrm{V}\right)\to \left(J{\upharpoonright }_{𝑡}X\right){\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}\left(X\cap A\right)$$
7	4 6	mpd3an3	$$⊢\left(J\in V\wedge A\in W\right)\to \left(J{\upharpoonright }_{𝑡}X\right){\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}\left(X\cap A\right)$$
8	1	restid	$$⊢J\in V\to J{\upharpoonright }_{𝑡}X=J$$
9	8	adantr	$$⊢\left(J\in V\wedge A\in W\right)\to J{\upharpoonright }_{𝑡}X=J$$
10	9	oveq1d	$$⊢\left(J\in V\wedge A\in W\right)\to \left(J{\upharpoonright }_{𝑡}X\right){\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}A$$
11		incom	$$⊢X\cap A=A\cap X$$
12	11	oveq2i	$$⊢J{\upharpoonright }_{𝑡}\left(X\cap A\right)=J{\upharpoonright }_{𝑡}\left(A\cap X\right)$$
13	12	a1i	$$⊢\left(J\in V\wedge A\in W\right)\to J{\upharpoonright }_{𝑡}\left(X\cap A\right)=J{\upharpoonright }_{𝑡}\left(A\cap X\right)$$
14	7 10 13	3eqtr3d	$$⊢\left(J\in V\wedge A\in W\right)\to J{\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}\left(A\cap X\right)$$