Metamath Proof Explorer

Theorem isros

Description: The property of being a rings of sets, i.e. containing the empty set, and closed under finite union and set complement. (Contributed by Thierry Arnoux, 18-Jul-2020)

Ref Expression
Hypothesis isros.1 ⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
Assertion isros ( 𝑆 ∈ 𝑄 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isros.1 ⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
2 eleq2 ⊢ ( 𝑠 = 𝑆 → ( ∅ ∈ 𝑠 ↔ ∅ ∈ 𝑆 ) )
3 eleq2 ⊢ ( 𝑠 = 𝑆 → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ↔ ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ) )
4 eleq2 ⊢ ( 𝑠 = 𝑆 → ( ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ↔ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) )
5 3 4 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ↔ ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) )
6 5 raleqbi1dv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ↔ ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) )
7 6 raleqbi1dv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) )
8 2 7 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) ↔ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) ) )
9 8 1 elrab2 ⊢ ( 𝑆 ∈ 𝑄 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) ) )
10 3anass ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) ) )
11 uneq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ∪ 𝑦 ) = ( 𝑢 ∪ 𝑦 ) )
12 11 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ↔ ( 𝑢 ∪ 𝑦 ) ∈ 𝑆 ) )
13 difeq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ∖ 𝑦 ) = ( 𝑢 ∖ 𝑦 ) )
14 13 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ↔ ( 𝑢 ∖ 𝑦 ) ∈ 𝑆 ) )
15 12 14 anbi12d ⊢ ( 𝑥 = 𝑢 → ( ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ↔ ( ( 𝑢 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑦 ) ∈ 𝑆 ) ) )
16 uneq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑢 ∪ 𝑦 ) = ( 𝑢 ∪ 𝑣 ) )
17 16 eleq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 ∪ 𝑦 ) ∈ 𝑆 ↔ ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ) )
18 difeq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑢 ∖ 𝑦 ) = ( 𝑢 ∖ 𝑣 ) )
19 18 eleq1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑢 ∖ 𝑦 ) ∈ 𝑆 ↔ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) )
20 17 19 anbi12d ⊢ ( 𝑦 = 𝑣 → ( ( ( 𝑢 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑦 ) ∈ 𝑆 ) ↔ ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ) )
21 15 20 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ↔ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) )
22 21 3anbi3i ⊢ ( ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑆 ) ) ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ) )
23 9 10 22 3bitr2i ⊢ ( 𝑆 ∈ 𝑄 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑆 ( ( 𝑢 ∪ 𝑣 ) ∈ 𝑆 ∧ ( 𝑢 ∖ 𝑣 ) ∈ 𝑆 ) ) )