df-salg

Description: Define the class of sigma-algebras. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	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))\}$

Step	Hyp	Ref	Expression
0		csalg	$class SAlg$
1		vx	$setvar x$
2		c0	$class \emptyset$
3	1	cv	$setvar x$
4	2 3	wcel	$wff \emptyset \in x$
5		vy	$setvar y$
6	3	cuni	$class ⋃ x$
7	5	cv	$setvar y$
8	6 7	cdif	$class (⋃ x ∖ y)$
9	8 3	wcel	$wff ⋃ x ∖ y \in x$
10	9 5 3	wral	$wff \forall y \in x ⋃ x ∖ y \in x$
11	3	cpw	$class 𝒫 x$
12		cdom	$class ≼$
13		com	$class ω$
14	7 13 12	wbr	$wff y ≼ ω$
15	7	cuni	$class ⋃ y$
16	15 3	wcel	$wff ⋃ y \in x$
17	14 16	wi	$wff (y ≼ ω \to ⋃ y \in x)$
18	17 5 11	wral	$wff \forall y \in 𝒫 x (y ≼ ω \to ⋃ y \in x)$
19	4 10 18	w3a	$wff (\emptyset \in x \land \forall y \in x ⋃ x ∖ y \in x \land \forall y \in 𝒫 x (y ≼ ω \to ⋃ y \in x))$
20	19 1	cab	$class \{x \| (\emptyset \in x \land \forall y \in x ⋃ x ∖ y \in x \land \forall y \in 𝒫 x (y ≼ ω \to ⋃ y \in x))\}$
21	0 20	wceq	$wff SAlg = \{x \| (\emptyset \in x \land \forall y \in x ⋃ x ∖ y \in x \land \forall y \in 𝒫 x (y ≼ ω \to ⋃ y \in x))\}$

Metamath Proof Explorer