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	$⊢ N = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cap y \in s \land \exists z \in 𝒫 s (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)))\}$
	Assertion	diffiunisros	$⊢ (S \in N \land A \in S \land B \in S) \to \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ B = ⋃ z)$

Proof

Step	Hyp	Ref	Expression
1		issros.1	$⊢ N = \{s \in 𝒫 𝒫 O \| (\emptyset \in s \land \forall x \in s \forall y \in s (x \cap y \in s \land \exists z \in 𝒫 s (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)))\}$
2		simp2	$⊢ (S \in N \land A \in S \land B \in S) \to A \in S$
3		simp3	$⊢ (S \in N \land A \in S \land B \in S) \to B \in S$
4	1	issros	$⊢ S \in N \leftrightarrow (S \in 𝒫 𝒫 O \land \emptyset \in S \land \forall x \in S \forall y \in S (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)))$
5	4	simp3bi	$⊢ S \in N \to \forall x \in S \forall y \in S (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z))$
6	5	3ad2ant1	$⊢ (S \in N \land A \in S \land B \in S) \to \forall x \in S \forall y \in S (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z))$
7		ineq1	$⊢ x = A \to x \cap y = A \cap y$
8	7	eleq1d	$⊢ x = A \to (x \cap y \in S \leftrightarrow A \cap y \in S)$
9		difeq1	$⊢ x = A \to x ∖ y = A ∖ y$
10	9	eqeq1d	$⊢ x = A \to (x ∖ y = ⋃ z \leftrightarrow A ∖ y = ⋃ z)$
11	10	3anbi3d	$⊢ x = A \to ((z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z) \leftrightarrow (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ y = ⋃ z))$
12	11	rexbidv	$⊢ x = A \to (\exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z) \leftrightarrow \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ y = ⋃ z))$
13	8 12	anbi12d	$⊢ x = A \to ((x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z)) \leftrightarrow (A \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ y = ⋃ z)))$
14		ineq2	$⊢ y = B \to A \cap y = A \cap B$
15	14	eleq1d	$⊢ y = B \to (A \cap y \in S \leftrightarrow A \cap B \in S)$
16		difeq2	$⊢ y = B \to A ∖ y = A ∖ B$
17	16	eqeq1d	$⊢ y = B \to (A ∖ y = ⋃ z \leftrightarrow A ∖ B = ⋃ z)$
18	17	3anbi3d	$⊢ y = B \to ((z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ y = ⋃ z) \leftrightarrow (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ B = ⋃ z))$
19	18	rexbidv	$⊢ y = B \to (\exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ y = ⋃ z) \leftrightarrow \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ B = ⋃ z))$
20	15 19	anbi12d	$⊢ y = B \to ((A \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ y = ⋃ z)) \leftrightarrow (A \cap B \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ B = ⋃ z)))$
21	13 20	rspc2va	$⊢ ((A \in S \land B \in S) \land \forall x \in S \forall y \in S (x \cap y \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land x ∖ y = ⋃ z))) \to (A \cap B \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ B = ⋃ z))$
22	2 3 6 21	syl21anc	$⊢ (S \in N \land A \in S \land B \in S) \to (A \cap B \in S \land \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ B = ⋃ z))$
23	22	simprd	$⊢ (S \in N \land A \in S \land B \in S) \to \exists z \in 𝒫 S (z \in Fin \land \underset{t \in z}{Disj} t \land A ∖ B = ⋃ z)$

Metamath Proof Explorer

Theorem diffiunisros

Proof