df-siga

Description: Define a sigma-algebra, i.e. a set closed under complement and countable union. Literature usually uses capital greek sigma and omega letters for the algebra set, and the base set respectively. We are using S and O as a parallel. (Contributed by Thierry Arnoux, 3-Sep-2016)

		Ref	Expression
	Assertion	df-siga	$⊢ sigAlgebra = (o \in V ⟼ \{s \| (s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csiga	$class sigAlgebra$
1		vo	$setvar o$
2		cvv	$class V$
3		vs	$setvar s$
4	3	cv	$setvar s$
5	1	cv	$setvar o$
6	5	cpw	$class 𝒫 o$
7	4 6	wss	$wff s \subseteq 𝒫 o$
8	5 4	wcel	$wff o \in s$
9		vx	$setvar x$
10	9	cv	$setvar x$
11	5 10	cdif	$class (o ∖ x)$
12	11 4	wcel	$wff o ∖ x \in s$
13	12 9 4	wral	$wff \forall x \in s o ∖ x \in s$
14	4	cpw	$class 𝒫 s$
15		cdom	$class ≼$
16		com	$class ω$
17	10 16 15	wbr	$wff x ≼ ω$
18	10	cuni	$class ⋃ x$
19	18 4	wcel	$wff ⋃ x \in s$
20	17 19	wi	$wff (x ≼ ω \to ⋃ x \in s)$
21	20 9 14	wral	$wff \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)$
22	8 13 21	w3a	$wff (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))$
23	7 22	wa	$wff (s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))$
24	23 3	cab	$class \{s \| (s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\}$
25	1 2 24	cmpt	$class (o \in V ⟼ \{s \| (s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\})$
26	0 25	wceq	$wff sigAlgebra = (o \in V ⟼ \{s \| (s \subseteq 𝒫 o \land (o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\})$

Metamath Proof Explorer

Definition df-siga

Detailed syntax breakdown