Metamath Proof Explorer

Theorem diffiunisros

Description: In semiring of sets, complements can be written as finite disjoint unions. (Contributed by Thierry Arnoux, 18-Jul-2020)

Ref Expression
Hypothesis issros.1 ⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
Assertion diffiunisros ( ( 𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 issros.1 ⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
2 simp2 ⊢ ( ( 𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐴 ∈ 𝑆 )
3 simp3 ⊢ ( ( 𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → 𝐵 ∈ 𝑆 )
4 1 issros ⊢ ( 𝑆 ∈ 𝑁 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
5 4 simp3bi ⊢ ( 𝑆 ∈ 𝑁 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) )
7 ineq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝐴 ∩ 𝑦 ) )
8 7 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ↔ ( 𝐴 ∩ 𝑦 ) ∈ 𝑆 ) )
9 difeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∖ 𝑦 ) = ( 𝐴 ∖ 𝑦 ) )
10 9 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ↔ ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ) )
11 10 3anbi3d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ↔ ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ) ) )
12 11 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ) ) )
13 8 12 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ↔ ( ( 𝐴 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
14 ineq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ 𝐵 ) )
15 14 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∩ 𝑦 ) ∈ 𝑆 ↔ ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 ) )
16 difeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ 𝐵 ) )
17 16 eqeq1d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ↔ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) )
18 17 3anbi3d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ) ↔ ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) ) )
19 18 rexbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) ) )
20 15 19 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝑦 ) = ∪ 𝑧 ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) ) ) )
21 13 20 rspc2va ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) ) )
22 2 3 6 21 syl21anc ⊢ ( ( 𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) ) )
23 22 simprd ⊢ ( ( 𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝐴 ∖ 𝐵 ) = ∪ 𝑧 ) )