Theorem issal

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

	Ref	Expression
Assertion	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 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( x = S -> ( (/) e. x <-> (/) e. S ) )
2		id	|- ( x = S -> x = S )
3		unieq	|- ( x = S -> U. x = U. S )
4	3	difeq1d	|- ( x = S -> ( U. x \ y ) = ( U. S \ y ) )
5	4 2	eleq12d	|- ( x = S -> ( ( U. x \ y ) e. x <-> ( U. S \ y ) e. S ) )
6	2 5	raleqbidv	|- ( x = S -> ( A. y e. x ( U. x \ y ) e. x <-> A. y e. S ( U. S \ y ) e. S ) )
7		pweq	|- ( x = S -> ~P x = ~P S )
8		eleq2	|- ( x = S -> ( U. y e. x <-> U. y e. S ) )
9	8	imbi2d	|- ( x = S -> ( ( y ~<_ _om -> U. y e. x ) <-> ( y ~<_ _om -> U. y e. S ) ) )
10	7 9	raleqbidv	|- ( x = S -> ( A. y e. ~P x ( y ~<_ _om -> U. y e. x ) <-> A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) )
11	1 6 10	3anbi123d	|- ( x = S -> ( ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ _om -> U. y e. x ) ) <-> ( (/) e. S /\ A. y e. S ( U. S \ y ) e. S /\ A. y e. ~P S ( y ~<_ _om -> U. y e. S ) ) ) )
12		df-salg	|- SAlg = { x | ( (/) e. x /\ A. y e. x ( U. x \ y ) e. x /\ A. y e. ~P x ( y ~<_ _om -> U. y e. x ) ) }
13	11 12	elab2g	|- ( 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 ) ) ) )