Theorem issald

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

	Ref	Expression
Hypotheses	issald.s	|- ( ph -> S e. V )
	issald.z	|- ( ph -> (/) e. S )
	issald.x	|- X = U. S
	issald.d	|- ( ( ph /\ y e. S ) -> ( X \ y ) e. S )
	issald.u	|- ( ( ph /\ y e. ~P S /\ y ~<_ _om ) -> U. y e. S )
Assertion	issald	|- ( ph -> S e. SAlg )

Proof

Step	Hyp	Ref	Expression
1		issald.s	|- ( ph -> S e. V )
2		issald.z	|- ( ph -> (/) e. S )
3		issald.x	|- X = U. S
4		issald.d	|- ( ( ph /\ y e. S ) -> ( X \ y ) e. S )
5		issald.u	|- ( ( ph /\ y e. ~P S /\ y ~<_ _om ) -> U. y e. S )
6	3	eqcomi	|- U. S = X
7	6	difeq1i	|- ( U. S \ y ) = ( X \ y )
8	7 4	eqeltrid	|- ( ( ph /\ y e. S ) -> ( U. S \ y ) e. S )
9	8	ralrimiva	|- ( ph -> A. y e. S ( U. S \ y ) e. S )
10	5	3expia	|- ( ( ph /\ y e. ~P S ) -> ( y ~<_ _om -> U. y e. S ) )
11	10	ralrimiva	|- ( ph -> A. y e. ~P S ( y ~<_ _om -> U. y e. S ) )
12		issal	|- ( S e. V -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
13	1 12	syl	|- ( ph -> ( S e. SAlg <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
14	2 9 11 13	mpbir3and	|- ( ph -> S e. SAlg )