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 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥𝑠𝑦𝑠 ( ( 𝑥𝑦 ) ∈ 𝑠 ∧ ( 𝑥𝑦 ) ∈ 𝑠 ) ) }
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 ( ( 𝑆𝑄𝐴𝑆𝐵𝑆 ) → ( 𝐴𝐵 ) ∈ 𝑆 )