Metamath Proof Explorer

Theorem sigaex

Description: Lemma for issiga and isrnsiga . The class of sigma-algebras with base set o is a set. Note: a more generic version with ( O e. _V -> ... ) could be useful for sigaval . (Contributed by Thierry Arnoux, 24-Oct-2016)

		Ref	Expression
	Assertion	sigaex	$⊢ \{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$

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		vex	$⊢ o \in V$
7		pwexg	$⊢ o \in V \to 𝒫 o \in V$
8		pwexg	$⊢ 𝒫 o \in V \to 𝒫 𝒫 o \in V$
9	6 7 8	mp2b	$⊢ 𝒫 𝒫 o \in V$
10	9	rabex	$⊢ \{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$
11	5 10	eqeltrri	$⊢ \{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$