Theorem issald

Description: Sufficient condition to prove that S is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	issald.s	$$⊢\phi \to S\in V$$
	issald.z	$$⊢\phi \to \varnothing \in S$$
	issald.x	$$⊢X=\bigcup S$$
	issald.d	$$⊢\left(\phi \wedge y\in S\right)\to X\setminus y\in S$$
	issald.u	$$⊢\left(\phi \wedge y\in 𝒫S\wedge y\preccurlyeq \mathrm{\omega }\right)\to \bigcup y\in S$$
Assertion	issald	$$⊢\phi \to S\in \mathrm{SAlg}$$

Proof

Step	Hyp	Ref	Expression
1		issald.s	$$⊢\phi \to S\in V$$
2		issald.z	$$⊢\phi \to \varnothing \in S$$
3		issald.x	$$⊢X=\bigcup S$$
4		issald.d	$$⊢\left(\phi \wedge y\in S\right)\to X\setminus y\in S$$
5		issald.u	$$⊢\left(\phi \wedge y\in 𝒫S\wedge y\preccurlyeq \mathrm{\omega }\right)\to \bigcup y\in S$$
6	3	eqcomi	$$⊢\bigcup S=X$$
7	6	difeq1i	$$⊢\bigcup S\setminus y=X\setminus y$$
8	7 4	eqeltrid	$$⊢\left(\phi \wedge y\in S\right)\to \bigcup S\setminus y\in S$$
9	8	ralrimiva	$$⊢\phi \to \forall y\in S\bigcup S\setminus y\in S$$
10	5	3expia	$$⊢\left(\phi \wedge y\in 𝒫S\right)\to \left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)$$
11	10	ralrimiva	$$⊢\phi \to \forall y\in 𝒫S\left(y\preccurlyeq \mathrm{\omega }\to \bigcup y\in S\right)$$
12		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)$$
13	1 12	syl	$$⊢\phi \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)$$
14	2 9 11 13	mpbir3and	$$⊢\phi \to S\in \mathrm{SAlg}$$