Theorem restuni2

Description: The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		restin.1	$$⊢X=\bigcup J$$
2		simpl	$$⊢\left(J\in \mathrm{Top}\wedge A\in V\right)\to J\in \mathrm{Top}$$
3		inss2	$$⊢A\cap X\subseteq X$$
4	1	restuni	$$⊢\left(J\in \mathrm{Top}\wedge A\cap X\subseteq X\right)\to A\cap X=\bigcup \left(J{\upharpoonright }_{𝑡}\left(A\cap X\right)\right)$$
5	2 3 4	sylancl	$$⊢\left(J\in \mathrm{Top}\wedge A\in V\right)\to A\cap X=\bigcup \left(J{\upharpoonright }_{𝑡}\left(A\cap X\right)\right)$$
6	1	restin	$$⊢\left(J\in \mathrm{Top}\wedge A\in V\right)\to J{\upharpoonright }_{𝑡}A=J{\upharpoonright }_{𝑡}\left(A\cap X\right)$$
7	6	unieqd	$$⊢\left(J\in \mathrm{Top}\wedge A\in V\right)\to \bigcup \left(J{\upharpoonright }_{𝑡}A\right)=\bigcup \left(J{\upharpoonright }_{𝑡}\left(A\cap X\right)\right)$$
8	5 7	eqtr4d	$$⊢\left(J\in \mathrm{Top}\wedge A\in V\right)\to A\cap X=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$