Theorem dmsigagen

Description: A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017)

	Ref	Expression
Assertion	dmsigagen	$$⊢\mathrm{dom}𝛔=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vuniex	$$⊢\bigcup j\in \mathrm{V}$$
2		pwsiga	$$⊢\bigcup j\in \mathrm{V}\to 𝒫\bigcup j\in \mathrm{sigAlgebra}\left(\bigcup j\right)$$
3	1 2	ax-mp	$$⊢𝒫\bigcup j\in \mathrm{sigAlgebra}\left(\bigcup j\right)$$
4		pwuni	$$⊢j\subseteq 𝒫\bigcup j$$
5		sseq2	$$⊢s=𝒫\bigcup j\to \left(j\subseteq s\leftrightarrow j\subseteq 𝒫\bigcup j\right)$$
6	5	rspcev	$$⊢\left(𝒫\bigcup j\in \mathrm{sigAlgebra}\left(\bigcup j\right)\wedge j\subseteq 𝒫\bigcup j\right)\to \exists s\in \mathrm{sigAlgebra}\left(\bigcup j\right)j\subseteq s$$
7	3 4 6	mp2an	$$⊢\exists s\in \mathrm{sigAlgebra}\left(\bigcup j\right)j\subseteq s$$
8		rabn0	$$⊢\left\{s\in \mathrm{sigAlgebra}\left(\bigcup j\right)|j\subseteq s\right\}\ne \varnothing \leftrightarrow \exists s\in \mathrm{sigAlgebra}\left(\bigcup j\right)j\subseteq s$$
9	7 8	mpbir	$$⊢\left\{s\in \mathrm{sigAlgebra}\left(\bigcup j\right)|j\subseteq s\right\}\ne \varnothing$$
10		intex	$$⊢\left\{s\in \mathrm{sigAlgebra}\left(\bigcup j\right)|j\subseteq s\right\}\ne \varnothing \leftrightarrow \bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup j\right)|j\subseteq s\right\}\in \mathrm{V}$$
11	9 10	mpbi	$$⊢\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup j\right)|j\subseteq s\right\}\in \mathrm{V}$$
12		df-sigagen	$$⊢𝛔=\left(j\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup j\right)|j\subseteq s\right\}\right)$$
13	11 12	dmmpti	$$⊢\mathrm{dom}𝛔=\mathrm{V}$$