Theorem srossspw

Description: A semiring of sets is a collection of subsets of O . (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	srossspw	|- ( S e. N -> S C_ ~P O )

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	1	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 ) ) ) )
3	2	simp1bi	|- ( S e. N -> S e. ~P ~P O )
4	3	elpwid	|- ( S e. N -> S C_ ~P O )