Metamath Proof Explorer

Theorem isros

Description: The property of being a rings of sets, i.e. containing the empty set, and closed under finite union and 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 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 ) ) )

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 eleq2 
 |-  ( s = S -> ( (/) e. s <-> (/) e. S ) )
3 eleq2 
 |-  ( s = S -> ( ( x u. y ) e. s <-> ( x u. y ) e. S ) )
4 eleq2 
 |-  ( s = S -> ( ( x \ y ) e. s <-> ( x \ y ) e. S ) )
5 3 4 anbi12d 
 |-  ( s = S -> ( ( ( x u. y ) e. s /\ ( x \ y ) e. s ) <-> ( ( x u. y ) e. S /\ ( x \ y ) e. S ) ) )
6 5 raleqbi1dv 
 |-  ( s = S -> ( A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) <-> A. y e. S ( ( x u. y ) e. S /\ ( x \ y ) e. S ) ) )
7 6 raleqbi1dv 
 |-  ( s = S -> ( A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) <-> A. x e. S A. y e. S ( ( x u. y ) e. S /\ ( x \ y ) e. S ) ) )
8 2 7 anbi12d 
 |-  ( s = S -> ( ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) <-> ( (/) e. S /\ A. x e. S A. y e. S ( ( x u. y ) e. S /\ ( x \ y ) e. S ) ) ) )
9 8 1 elrab2 
 |-  ( S e. 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 ) ) ) )
10 3anass 
 |-  ( ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x u. y ) e. S /\ ( x \ y ) e. S ) ) <-> ( S e. ~P ~P O /\ ( (/) e. S /\ A. x e. S A. y e. S ( ( x u. y ) e. S /\ ( x \ y ) e. S ) ) ) )
11 uneq1 
 |-  ( x = u -> ( x u. y ) = ( u u. y ) )
12 11 eleq1d 
 |-  ( x = u -> ( ( x u. y ) e. S <-> ( u u. y ) e. S ) )
13 difeq1 
 |-  ( x = u -> ( x \ y ) = ( u \ y ) )
14 13 eleq1d 
 |-  ( x = u -> ( ( x \ y ) e. S <-> ( u \ y ) e. S ) )
15 12 14 anbi12d 
 |-  ( x = u -> ( ( ( x u. y ) e. S /\ ( x \ y ) e. S ) <-> ( ( u u. y ) e. S /\ ( u \ y ) e. S ) ) )
16 uneq2 
 |-  ( y = v -> ( u u. y ) = ( u u. v ) )
17 16 eleq1d 
 |-  ( y = v -> ( ( u u. y ) e. S <-> ( u u. v ) e. S ) )
18 difeq2 
 |-  ( y = v -> ( u \ y ) = ( u \ v ) )
19 18 eleq1d 
 |-  ( y = v -> ( ( u \ y ) e. S <-> ( u \ v ) e. S ) )
20 17 19 anbi12d 
 |-  ( y = v -> ( ( ( u u. y ) e. S /\ ( u \ y ) e. S ) <-> ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) )
21 15 20 cbvral2vw 
 |-  ( A. x e. S A. y e. S ( ( x u. y ) e. S /\ ( x \ y ) e. S ) <-> A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) )
22 21 3anbi3i 
 |-  ( ( S e. ~P ~P O /\ (/) e. S /\ A. x e. S A. y e. S ( ( x u. y ) e. S /\ ( x \ y ) e. S ) ) <-> ( S e. ~P ~P O /\ (/) e. S /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) )
23 9 10 22 3bitr2i 
 |-  ( 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 ) ) )