issros

Description: The property of being a semirings of sets, i.e., collections of sets containing the empty set, closed under finite intersection, and where 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	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)))$

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		eleq2	$⊢ s = S \to (\emptyset \in s \leftrightarrow \emptyset \in S)$
3		eleq2	$⊢ s = S \to (x \cap y \in s \leftrightarrow x \cap y \in S)$
4		pweq	$⊢ s = S \to 𝒫 s = 𝒫 S$
5	4	rexeqdv	$⊢ s = S \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 x ∖ y = ⋃ z))$
6	3 5	anbi12d	$⊢ s = S \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 (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	6	raleqbi1dv	$⊢ s = S \to (\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)) \leftrightarrow \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)))$
8	7	raleqbi1dv	$⊢ s = 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)) \leftrightarrow \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)))$
9	2 8	anbi12d	$⊢ s = S \to ((\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))) \leftrightarrow (\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))))$
10	9 1	elrab2	$⊢ 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))))$
11		3anass	$⊢ (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))) \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))))$
12	10 11	bitr4i	$⊢ 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)))$

Metamath Proof Explorer

Theorem issros

Proof