Metamath Proof Explorer

Theorem isrnsiga

Description: The property of being a sigma-algebra on an indefinite base set. (Contributed by Thierry Arnoux, 3-Sep-2016) (Proof shortened by Thierry Arnoux, 23-Oct-2016)

		Ref	Expression
	Assertion	isrnsiga	$⊢ S \in ⋃ ran sigAlgebra \leftrightarrow (S \in V \land \exists o (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-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)))\})$
2		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$
3		sseq1	$⊢ s = S \to (s \subseteq 𝒫 o \leftrightarrow S \subseteq 𝒫 o)$
4		eleq2	$⊢ s = S \to (o \in s \leftrightarrow o \in S)$
5		eleq2	$⊢ s = S \to (o ∖ x \in s \leftrightarrow o ∖ x \in S)$
6	5	raleqbi1dv	$⊢ s = S \to (\forall x \in s o ∖ x \in s \leftrightarrow \forall x \in S o ∖ x \in S)$
7		pweq	$⊢ s = S \to 𝒫 s = 𝒫 S$
8		eleq2	$⊢ s = S \to (⋃ x \in s \leftrightarrow ⋃ x \in S)$
9	8	imbi2d	$⊢ s = S \to ((x ≼ ω \to ⋃ x \in s) \leftrightarrow (x ≼ ω \to ⋃ x \in S))$
10	7 9	raleqbidv	$⊢ s = S \to (\forall x \in 𝒫 s (x ≼ ω \to ⋃ x \in s) \leftrightarrow \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
11	4 6 10	3anbi123d	$⊢ s = S \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)))$
12	3 11	anbi12d	$⊢ s = S \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))))$
13	1 2 12	abfmpunirn	$⊢ S \in ⋃ ran sigAlgebra \leftrightarrow (S \in V \land \exists o \in V (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))))$
14		rexv	$⊢ \exists o \in V (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 \exists o (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)))$
15	14	anbi2i	$⊢ (S \in V \land \exists o \in V (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 \in V \land \exists o (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))))$
16	13 15	bitri	$⊢ S \in ⋃ ran sigAlgebra \leftrightarrow (S \in V \land \exists o (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))))$