Theorem rossspw

Description: A ring of sets is a collection of subsets of O . (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypothesis	isros.1	|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
Assertion	rossspw	|- ( S e. Q -> S C_ ~P O )

Proof

Step	Hyp	Ref	Expression
1		isros.1	|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) }
2	1	isros	|- ( S e. Q <-> ( S e. ~P ~P O /\ (/) e. S /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) )
3	2	simp1bi	|- ( S e. Q -> S e. ~P ~P O )
4	3	elpwid	|- ( S e. Q -> S C_ ~P O )