Theorem bj-restuni2

Description: The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni and restuni2 . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restuni2	$$⊢\left(X\in V\wedge A\subseteq \bigcup X\right)\to \bigcup \left(X{\upharpoonright }_{𝑡}A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$$⊢X\in V\to \bigcup X\in \mathrm{V}$$
2		ssexg	$$⊢\left(A\subseteq \bigcup X\wedge \bigcup X\in \mathrm{V}\right)\to A\in \mathrm{V}$$
3	1 2	sylan2	$$⊢\left(A\subseteq \bigcup X\wedge X\in V\right)\to A\in \mathrm{V}$$
4	3	ancoms	$$⊢\left(X\in V\wedge A\subseteq \bigcup X\right)\to A\in \mathrm{V}$$
5		bj-restuni	$$⊢\left(X\in V\wedge A\in \mathrm{V}\right)\to \bigcup \left(X{\upharpoonright }_{𝑡}A\right)=\bigcup X\cap A$$
6	4 5	syldan	$$⊢\left(X\in V\wedge A\subseteq \bigcup X\right)\to \bigcup \left(X{\upharpoonright }_{𝑡}A\right)=\bigcup X\cap A$$
7		inss2	$$⊢\bigcup X\cap A\subseteq A$$
8	7	a1i	$$⊢A\subseteq \bigcup X\to \bigcup X\cap A\subseteq A$$
9		id	$$⊢A\subseteq \bigcup X\to A\subseteq \bigcup X$$
10		ssidd	$$⊢A\subseteq \bigcup X\to A\subseteq A$$
11	9 10	ssind	$$⊢A\subseteq \bigcup X\to A\subseteq \bigcup X\cap A$$
12	8 11	eqssd	$$⊢A\subseteq \bigcup X\to \bigcup X\cap A=A$$
13	12	adantl	$$⊢\left(X\in V\wedge A\subseteq \bigcup X\right)\to \bigcup X\cap A=A$$
14	6 13	eqtrd	$$⊢\left(X\in V\wedge A\subseteq \bigcup X\right)\to \bigcup \left(X{\upharpoonright }_{𝑡}A\right)=A$$