issal

Description: Express the predicate " S is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	issal	$⊢ S \in V \to (S \in SAlg \leftrightarrow (\emptyset \in S \land \forall y \in S ⋃ S ∖ y \in S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)))$

Step	Hyp	Ref	Expression
1		eleq2	$⊢ x = S \to (\emptyset \in x \leftrightarrow \emptyset \in S)$
2		id	$⊢ x = S \to x = S$
3		unieq	$⊢ x = S \to ⋃ x = ⋃ S$
4	3	difeq1d	$⊢ x = S \to ⋃ x ∖ y = ⋃ S ∖ y$
5	4 2	eleq12d	$⊢ x = S \to (⋃ x ∖ y \in x \leftrightarrow ⋃ S ∖ y \in S)$
6	2 5	raleqbidv	$⊢ x = S \to (\forall y \in x ⋃ x ∖ y \in x \leftrightarrow \forall y \in S ⋃ S ∖ y \in S)$
7		pweq	$⊢ x = S \to 𝒫 x = 𝒫 S$
8		eleq2	$⊢ x = S \to (⋃ y \in x \leftrightarrow ⋃ y \in S)$
9	8	imbi2d	$⊢ x = S \to ((y ≼ ω \to ⋃ y \in x) \leftrightarrow (y ≼ ω \to ⋃ y \in S))$
10	7 9	raleqbidv	$⊢ x = S \to (\forall y \in 𝒫 x (y ≼ ω \to ⋃ y \in x) \leftrightarrow \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S))$
11	1 6 10	3anbi123d	$⊢ x = S \to ((\emptyset \in x \land \forall y \in x ⋃ x ∖ y \in x \land \forall y \in 𝒫 x (y ≼ ω \to ⋃ y \in x)) \leftrightarrow (\emptyset \in S \land \forall y \in S ⋃ S ∖ y \in S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)))$
12		df-salg	$⊢ SAlg = \{x \| (\emptyset \in x \land \forall y \in x ⋃ x ∖ y \in x \land \forall y \in 𝒫 x (y ≼ ω \to ⋃ y \in x))\}$
13	11 12	elab2g	$⊢ S \in V \to (S \in SAlg \leftrightarrow (\emptyset \in S \land \forall y \in S ⋃ S ∖ y \in S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)))$

Metamath Proof Explorer