Metamath Proof Explorer


Theorem unelros

Description: A ring of sets is closed under union. (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 unelros
|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A u. 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 simpld
 |-  ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A u. B ) e. S )