Theorem isrnsigau

Description: The property of being a sigma-algebra, universe is the union set. (Contributed by Thierry Arnoux, 11-Nov-2016)

	Ref	Expression
Assertion	isrnsigau	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(S\subseteq 𝒫\bigcup S\wedge \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sgon	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to S\in \mathrm{sigAlgebra}\left(\bigcup S\right)$$
2		elex	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to S\in \mathrm{V}$$
3		issiga	$$⊢S\in \mathrm{V}\to \left(S\in \mathrm{sigAlgebra}\left(\bigcup S\right)\leftrightarrow \left(S\subseteq 𝒫\bigcup S\wedge \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)\right)\right)$$
4	2 3	syl	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(S\in \mathrm{sigAlgebra}\left(\bigcup S\right)\leftrightarrow \left(S\subseteq 𝒫\bigcup S\wedge \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)\right)\right)$$
5	1 4	mpbid	$$⊢S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(S\subseteq 𝒫\bigcup S\wedge \left(\bigcup S\in S\wedge \forall x\in S\bigcup S\setminus x\in S\wedge \forall x\in 𝒫S\left(x\preccurlyeq \mathrm{\omega }\to \bigcup x\in S\right)\right)\right)$$