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 𝒫 𝒫 O | s x s y s x y s x y s
Assertion unelros S Q A S B S A B S

Proof

Step Hyp Ref Expression
1 isros.1 Q = s 𝒫 𝒫 O | s x s y s x y s x y s
2 simp2 S Q A S B S A S
3 simp3 S Q A S B S B S
4 1 isros S Q S 𝒫 𝒫 O S u S v S u v S u v S
5 4 simp3bi S Q u S v S u v S u v S
6 5 3ad2ant1 S Q A S B S u S v S u v S u v S
7 uneq1 u = A u v = A v
8 7 eleq1d u = A u v S A v S
9 difeq1 u = A u v = A v
10 9 eleq1d u = A u v S A v S
11 8 10 anbi12d u = A u v S u v S A v S A v S
12 uneq2 v = B A v = A B
13 12 eleq1d v = B A v S A B S
14 difeq2 v = B A v = A B
15 14 eleq1d v = B A v S A B S
16 13 15 anbi12d v = B A v S A v S A B S A B S
17 11 16 rspc2va A S B S u S v S u v S u v S A B S A B S
18 2 3 6 17 syl21anc S Q A S B S A B S A B S
19 18 simpld S Q A S B S A B S