Theorem restuni6

Description: The underlying set of a subspace topology. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	restuni6.1	$$⊢\phi \to A\in V$$
	restuni6.2	$$⊢\phi \to B\in W$$
Assertion	restuni6	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)=\bigcup A\cap B$$

Proof

Step	Hyp	Ref	Expression
1		restuni6.1	$$⊢\phi \to A\in V$$
2		restuni6.2	$$⊢\phi \to B\in W$$
3		eqid	$$⊢\bigcup A=\bigcup A$$
4	3	restin	$$⊢\left(A\in V\wedge B\in W\right)\to A{\upharpoonright }_{𝑡}B=A{\upharpoonright }_{𝑡}\left(B\cap \bigcup A\right)$$
5	1 2 4	syl2anc	$$⊢\phi \to A{\upharpoonright }_{𝑡}B=A{\upharpoonright }_{𝑡}\left(B\cap \bigcup A\right)$$
6	5	unieqd	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)=\bigcup \left(A{\upharpoonright }_{𝑡}\left(B\cap \bigcup A\right)\right)$$
7		inss2	$$⊢B\cap \bigcup A\subseteq \bigcup A$$
8	7	a1i	$$⊢\phi \to B\cap \bigcup A\subseteq \bigcup A$$
9	1 8	restuni4	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}\left(B\cap \bigcup A\right)\right)=B\cap \bigcup A$$
10		incom	$$⊢B\cap \bigcup A=\bigcup A\cap B$$
11	10	a1i	$$⊢\phi \to B\cap \bigcup A=\bigcup A\cap B$$
12	6 9 11	3eqtrd	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)=\bigcup A\cap B$$