Theorem restuni4

Description: The underlying set of a subspace induced by the ` |``t ` operator. The result can be applied, for instance, to topologies and sigma-algebras. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		restuni4.1	$$⊢\phi \to A\in V$$
2		restuni4.2	$$⊢\phi \to B\subseteq \bigcup A$$
3		incom	$$⊢B\cap \bigcup A=\bigcup A\cap B$$
4	3	a1i	$$⊢\phi \to B\cap \bigcup A=\bigcup A\cap B$$
5		dfss	$$⊢B\subseteq \bigcup A\leftrightarrow B=B\cap \bigcup A$$
6	2 5	sylib	$$⊢\phi \to B=B\cap \bigcup A$$
7	1	uniexd	$$⊢\phi \to \bigcup A\in \mathrm{V}$$
8	7 2	ssexd	$$⊢\phi \to B\in \mathrm{V}$$
9	1 8	restuni3	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)=\bigcup A\cap B$$
10	4 6 9	3eqtr4rd	$$⊢\phi \to \bigcup \left(A{\upharpoonright }_{𝑡}B\right)=B$$