Theorem subsaluni

Description: A set belongs to the subspace sigma-algebra it induces. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	subsaluni.1	$$⊢\phi \to S\in \mathrm{SAlg}$$
	subsaluni.2	$$⊢\phi \to A\subseteq \bigcup S$$
Assertion	subsaluni	$$⊢\phi \to A\in \left(S{\upharpoonright }_{𝑡}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		subsaluni.1	$$⊢\phi \to S\in \mathrm{SAlg}$$
2		subsaluni.2	$$⊢\phi \to A\subseteq \bigcup S$$
3	1 2	restuni4	$$⊢\phi \to \bigcup \left(S{\upharpoonright }_{𝑡}A\right)=A$$
4	3	eqcomd	$$⊢\phi \to A=\bigcup \left(S{\upharpoonright }_{𝑡}A\right)$$
5	1	uniexd	$$⊢\phi \to \bigcup S\in \mathrm{V}$$
6	5 2	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
7		eqid	$$⊢S{\upharpoonright }_{𝑡}A=S{\upharpoonright }_{𝑡}A$$
8	1 6 7	subsalsal	$$⊢\phi \to S{\upharpoonright }_{𝑡}A\in \mathrm{SAlg}$$
9	8	salunid	$$⊢\phi \to \bigcup \left(S{\upharpoonright }_{𝑡}A\right)\in \left(S{\upharpoonright }_{𝑡}A\right)$$
10	4 9	eqeltrd	$$⊢\phi \to A\in \left(S{\upharpoonright }_{𝑡}A\right)$$