Theorem restuni5

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
Hypothesis	restuni5.1	$$⊢X=\bigcup J$$
Assertion	restuni5	$$⊢\left(J\in V\wedge A\subseteq X\right)\to A=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		restuni5.1	$$⊢X=\bigcup J$$
2		simpl	$$⊢\left(J\in V\wedge A\subseteq X\right)\to J\in V$$
3		id	$$⊢A\subseteq X\to A\subseteq X$$
4	3 1	sseqtrdi	$$⊢A\subseteq X\to A\subseteq \bigcup J$$
5	4	adantl	$$⊢\left(J\in V\wedge A\subseteq X\right)\to A\subseteq \bigcup J$$
6	2 5	restuni4	$$⊢\left(J\in V\wedge A\subseteq X\right)\to \bigcup \left(J{\upharpoonright }_{𝑡}A\right)=A$$
7	6	eqcomd	$$⊢\left(J\in V\wedge A\subseteq X\right)\to A=\bigcup \left(J{\upharpoonright }_{𝑡}A\right)$$