Theorem elsigass

Description: An element of a sigma-algebra is a subset of the base set. (Contributed by Thierry Arnoux, 6-Jun-2017)

	Ref	Expression
Assertion	elsigass	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\right)\to A\subseteq \bigcup S$$

Proof

Step	Hyp	Ref	Expression
1		sgon	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to S\in \mathrm{sigAlgebra}\left(\bigcup S\right)$$
2		sigasspw	$$⊢S\in \mathrm{sigAlgebra}\left(\bigcup S\right)\to S\subseteq 𝒫\bigcup S$$
3	1 2	syl	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to S\subseteq 𝒫\bigcup S$$
4	3	sselda	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\right)\to A\in 𝒫\bigcup S$$
5	4	elpwid	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge A\in S\right)\to A\subseteq \bigcup S$$