Theorem difelros

Description: A ring of sets is closed under set complement. (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	difelros	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )

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		simp2	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> A e. S )
3		simp3	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> B e. S )
4	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 ) ) )
5	4	simp3bi	|- ( S e. Q -> A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) )
6	5	3ad2ant1	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) )
7		uneq1	|- ( u = A -> ( u u. v ) = ( A u. v ) )
8	7	eleq1d	|- ( u = A -> ( ( u u. v ) e. S <-> ( A u. v ) e. S ) )
9		difeq1	|- ( u = A -> ( u \ v ) = ( A \ v ) )
10	9	eleq1d	|- ( u = A -> ( ( u \ v ) e. S <-> ( A \ v ) e. S ) )
11	8 10	anbi12d	|- ( u = A -> ( ( ( u u. v ) e. S /\ ( u \ v ) e. S ) <-> ( ( A u. v ) e. S /\ ( A \ v ) e. S ) ) )
12		uneq2	|- ( v = B -> ( A u. v ) = ( A u. B ) )
13	12	eleq1d	|- ( v = B -> ( ( A u. v ) e. S <-> ( A u. B ) e. S ) )
14		difeq2	|- ( v = B -> ( A \ v ) = ( A \ B ) )
15	14	eleq1d	|- ( v = B -> ( ( A \ v ) e. S <-> ( A \ B ) e. S ) )
16	13 15	anbi12d	|- ( v = B -> ( ( ( A u. v ) e. S /\ ( A \ v ) e. S ) <-> ( ( A u. B ) e. S /\ ( A \ B ) e. S ) ) )
17	11 16	rspc2va	|- ( ( ( A e. S /\ B e. S ) /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) -> ( ( A u. B ) e. S /\ ( A \ B ) e. S ) )
18	2 3 6 17	syl21anc	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( ( A u. B ) e. S /\ ( A \ B ) e. S ) )
19	18	simprd	|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A \ B ) e. S )