Theorem issal

Description: Express the predicate " S is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	issal	$$⊢S\in V\to \left(S\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq2w	$$⊢x=z\to \left(\varnothing \in x\leftrightarrow \varnothing \in z\right)$$
2		id	$$⊢x=z\to x=z$$
3		unieq	$$⊢x=z\to \bigcup x=\bigcup z$$
4	3	difeq1d	$$⊢x=z\to \bigcup x\setminus y=\bigcup z\setminus y$$
5	4 2	eleq12d	$$⊢x=z\to \left(\bigcup x\setminus y\in x\leftrightarrow \bigcup z\setminus y\in z\right)$$
6	2 5	raleqbidv	$$⊢x=z\to \left(\forall y\in x\bigcup x\setminus y\in x\leftrightarrow \forall y\in z\bigcup z\setminus y\in z\right)$$
7		pweq	$$⊢x=z\to 𝒫x=𝒫z$$
8		eleq2w	$$⊢x=z\to \left(\bigcup y\in x\leftrightarrow \bigcup y\in z\right)$$
9	8	imbi2d	$$⊢x=z\to \left(\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in x\right)\leftrightarrow \left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in z\right)\right)$$
10	7 9	raleqbidv	$$⊢x=z\to \left(\forall y\in 𝒫x\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in x\right)\leftrightarrow \forall y\in 𝒫z\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in z\right)\right)$$
11	1 6 10	3anbi123d	$$⊢x=z\to \left(\left(\varnothing \in x\wedge \forall y\in x\bigcup x\setminus y\in x\wedge \forall y\in 𝒫x\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in x\right)\right)\leftrightarrow \left(\varnothing \in z\wedge \forall y\in z\bigcup z\setminus y\in z\wedge \forall y\in 𝒫z\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in z\right)\right)\right)$$
12		eleq2	$$⊢z=S\to \left(\varnothing \in z\leftrightarrow \varnothing \in S\right)$$
13		id	$$⊢z=S\to z=S$$
14		unieq	$$⊢z=S\to \bigcup z=\bigcup S$$
15	14	difeq1d	$$⊢z=S\to \bigcup z\setminus y=\bigcup S\setminus y$$
16	15 13	eleq12d	$$⊢z=S\to \left(\bigcup z\setminus y\in z\leftrightarrow \bigcup S\setminus y\in S\right)$$
17	13 16	raleqbidv	$$⊢z=S\to \left(\forall y\in z\bigcup z\setminus y\in z\leftrightarrow \forall y\in S\bigcup S\setminus y\in S\right)$$
18		pweq	$$⊢z=S\to 𝒫z=𝒫S$$
19		eleq2	$$⊢z=S\to \left(\bigcup y\in z\leftrightarrow \bigcup y\in S\right)$$
20	19	imbi2d	$$⊢z=S\to \left(\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in z\right)\leftrightarrow \left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)$$
21	18 20	raleqbidv	$$⊢z=S\to \left(\forall y\in 𝒫z\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in z\right)\leftrightarrow \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)$$
22	12 17 21	3anbi123d	$$⊢z=S\to \left(\left(\varnothing \in z\wedge \forall y\in z\bigcup z\setminus y\in z\wedge \forall y\in 𝒫z\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in z\right)\right)\leftrightarrow \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)\right)$$
23		df-salg	$$⊢\mathrm{SAlg}=\left\{x|\left(\varnothing \in x\wedge \forall y\in x\bigcup x\setminus y\in x\wedge \forall y\in 𝒫x\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in x\right)\right)\right\}$$
24	11 22 23	elab2gw	$$⊢S\in V\to \left(S\in \mathrm{SAlg}\leftrightarrow \left(\varnothing \in S\wedge \forall y\in S\bigcup S\setminus y\in S\wedge \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)\right)\right)$$