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 𝑡𝑧 𝑡 ∧ ( 𝐴𝐵 ) = 𝑧 ) )