Theorem sigagenval

Description: Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

	Ref	Expression
Assertion	sigagenval	$$⊢A\in V\to 𝛔\left(A\right)=\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-sigagen	$$⊢𝛔=\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup x\right)|x\subseteq s\right\}\right)$$
2	1	a1i	$$⊢A\in V\to 𝛔=\left(x\in \mathrm{V}⟼\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup x\right)|x\subseteq s\right\}\right)$$
3		unieq	$$⊢x=A\to \bigcup x=\bigcup A$$
4	3	fveq2d	$$⊢x=A\to \mathrm{sigAlgebra}\left(\bigcup x\right)=\mathrm{sigAlgebra}\left(\bigcup A\right)$$
5		sseq1	$$⊢x=A\to \left(x\subseteq s\leftrightarrow A\subseteq s\right)$$
6	4 5	rabeqbidv	$$⊢x=A\to \left\{s\in \mathrm{sigAlgebra}\left(\bigcup x\right)|x\subseteq s\right\}=\left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$
7	6	inteqd	$$⊢x=A\to \bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup x\right)|x\subseteq s\right\}=\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$
8	7	adantl	$$⊢\left(A\in V\wedge x=A\right)\to \bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup x\right)|x\subseteq s\right\}=\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$
9		elex	$$⊢A\in V\to A\in \mathrm{V}$$
10		uniexg	$$⊢A\in V\to \bigcup A\in \mathrm{V}$$
11		pwsiga	$$⊢\bigcup A\in \mathrm{V}\to 𝒫\bigcup A\in \mathrm{sigAlgebra}\left(\bigcup A\right)$$
12	10 11	syl	$$⊢A\in V\to 𝒫\bigcup A\in \mathrm{sigAlgebra}\left(\bigcup A\right)$$
13		pwuni	$$⊢A\subseteq 𝒫\bigcup A$$
14	12 13	jctir	$$⊢A\in V\to \left(𝒫\bigcup A\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq 𝒫\bigcup A\right)$$
15		sseq2	$$⊢s=𝒫\bigcup A\to \left(A\subseteq s\leftrightarrow A\subseteq 𝒫\bigcup A\right)$$
16	15	elrab	$$⊢𝒫\bigcup A\in \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}\leftrightarrow \left(𝒫\bigcup A\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq 𝒫\bigcup A\right)$$
17	14 16	sylibr	$$⊢A\in V\to 𝒫\bigcup A\in \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$
18	17	ne0d	$$⊢A\in V\to \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}\ne \varnothing$$
19		intex	$$⊢\left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}\ne \varnothing \leftrightarrow \bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}\in \mathrm{V}$$
20	18 19	sylib	$$⊢A\in V\to \bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}\in \mathrm{V}$$
21	2 8 9 20	fvmptd	$$⊢A\in V\to 𝛔\left(A\right)=\bigcap \left\{s\in \mathrm{sigAlgebra}\left(\bigcup A\right)|A\subseteq s\right\}$$