Theorem issros

Description: The property of being a semirings of sets, i.e., collections of sets containing the empty set, closed under finite intersection, and where complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypothesis	issros.1	|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) }
Assertion	issros	|- ( S e. N <-> ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		issros.1	|- N = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) }
2		eleq2	|- ( s = S -> ( (/) e. s <-> (/) e. S ) )
3		eleq2	|- ( s = S -> ( ( x i^i y ) e. s <-> ( x i^i y ) e. S ) )
4		pweq	|- ( s = S -> ~P s = ~P S )
5	4	rexeqdv	|- ( s = S -> ( E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) <-> E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) )
6	3 5	anbi12d	|- ( s = S -> ( ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) <-> ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )
7	6	raleqbi1dv	|- ( s = S -> ( A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) <-> A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )
8	7	raleqbi1dv	|- ( s = S -> ( A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) <-> A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )
9	2 8	anbi12d	|- ( s = S -> ( ( (/) e. s /\ A. x e. s A. y e. s ( ( x i^i y ) e. s /\ E. z e. ~P s ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) <-> ( (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) ) )
10	9 1	elrab2	|- ( S e. N <-> ( S e. ~P ~P O /\ ( (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) ) )
11		3anass	|- ( ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) <-> ( S e. ~P ~P O /\ ( (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) ) )
12	10 11	bitr4i	|- ( S e. N <-> ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x i^i y ) e. S /\ E. z e. ~P S ( z e. Fin /\ Disj_ t e. z t /\ ( x \ y ) = U. z ) ) ) )