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