sigaval

Description: The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016)

		Ref	Expression
	Assertion	sigaval	$⊢ O \in V \to sigAlgebra (O) = \{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)))\}$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{s \in 𝒫 𝒫 O \| (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))\} = \{s \| (s \in 𝒫 𝒫 O \land (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\}$
2		velpw	$⊢ s \in 𝒫 𝒫 O \leftrightarrow s \subseteq 𝒫 O$
3	2	anbi1i	$⊢ (s \in 𝒫 𝒫 O \land (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))) \leftrightarrow (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)))$
4	3	abbii	$⊢ \{s \| (s \in 𝒫 𝒫 O \land (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))\} = \{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)))\}$
5	1 4	eqtri	$⊢ \{s \in 𝒫 𝒫 O \| (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))\} = \{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)))\}$
6		pwexg	$⊢ O \in V \to 𝒫 O \in V$
7		pwexg	$⊢ 𝒫 O \in V \to 𝒫 𝒫 O \in V$
8		rabexg	$⊢ 𝒫 𝒫 O \in V \to \{s \in 𝒫 𝒫 O \| (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))\} \in V$
9	6 7 8	3syl	$⊢ O \in V \to \{s \in 𝒫 𝒫 O \| (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s))\} \in V$
10	5 9	eqeltrrid	$⊢ O \in V \to \{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)))\} \in V$
11		pweq	$⊢ o = O \to 𝒫 o = 𝒫 O$
12	11	sseq2d	$⊢ o = O \to (s \subseteq 𝒫 o \leftrightarrow s \subseteq 𝒫 O)$
13		eleq1	$⊢ o = O \to (o \in s \leftrightarrow O \in s)$
14		difeq1	$⊢ o = O \to o ∖ x = O ∖ x$
15	14	eleq1d	$⊢ o = O \to (o ∖ x \in s \leftrightarrow O ∖ x \in s)$
16	15	ralbidv	$⊢ o = O \to (\forall x \in s o ∖ x \in s \leftrightarrow \forall x \in s O ∖ x \in s)$
17	13 16	3anbi12d	$⊢ o = O \to ((o \in s \land \forall x \in s o ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)) \leftrightarrow (O \in s \land \forall x \in s O ∖ x \in s \land \forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s)))$
18	12 17	anbi12d	$⊢ o = O \to ((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))) \leftrightarrow (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))))$
19	18	abbidv	$⊢ o = O \to \{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)))\} = \{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)))\}$
20		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)))\})$
21	19 20	fvmptg	$⊢ (O \in V \land \{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)))\} \in V) \to sigAlgebra (O) = \{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)))\}$
22	10 21	mpdan	$⊢ O \in V \to sigAlgebra (O) = \{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

Theorem sigaval

Proof