Theorem unelros

Description: A ring of sets is closed under union. (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypothesis	isros.1	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
Assertion	unelros	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		isros.1	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
2		simp2	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
3		simp3	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
4	1	isros	⊢ ( 𝑆 ∈ 𝑄 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ) )
5	4	simp3bi	⊢ ( 𝑆 ∈ 𝑄 → ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) )
6	5	3ad2ant1	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) )
7		uneq1	⊢ ( 𝑢 = 𝐴 → ( 𝑢 ∪ 𝑣 ) = ( 𝐴 ∪ 𝑣 ) )
8	7	eleq1d	⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ↔ ( 𝐴 ∪ 𝑣 ) ∈ 𝑆 ) )
9		difeq1	⊢ ( 𝑢 = 𝐴 → ( 𝑢 ∖ 𝑣 ) = ( 𝐴 ∖ 𝑣 ) )
10	9	eleq1d	⊢ ( 𝑢 = 𝐴 → ( ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ↔ ( 𝐴 ∖ 𝑣 ) ∈ 𝑆 ) )
11	8 10	anbi12d	⊢ ( 𝑢 = 𝐴 → ( ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ↔ ( ( 𝐴 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝐴 ∖ 𝑣 ) ∈ 𝑆 ) ) )
12		uneq2	⊢ ( 𝑣 = 𝐵 → ( 𝐴 ∪ 𝑣 ) = ( 𝐴 ∪ 𝐵 ) )
13	12	eleq1d	⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ∪ 𝑣 ) ∈ 𝑆 ↔ ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 ) )
14		difeq2	⊢ ( 𝑣 = 𝐵 → ( 𝐴 ∖ 𝑣 ) = ( 𝐴 ∖ 𝐵 ) )
15	14	eleq1d	⊢ ( 𝑣 = 𝐵 → ( ( 𝐴 ∖ 𝑣 ) ∈ 𝑆 ↔ ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ) )
16	13 15	anbi12d	⊢ ( 𝑣 = 𝐵 → ( ( ( 𝐴 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝐴 ∖ 𝑣 ) ∈ 𝑆 ) ↔ ( ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 ∧ ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ) ) )
17	11 16	rspc2va	⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ) → ( ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 ∧ ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ) )
18	2 3 6 17	syl21anc	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 ∧ ( 𝐴 ∖ 𝐵 ) ∈ 𝑆 ) )
19	18	simpld	⊢ ( ( 𝑆 ∈ 𝑄 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )