Metamath Proof Explorer

Theorem sigaclcu

Description: A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016)

		Ref	Expression
	Assertion	sigaclcu	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A ≼ ω) \to ⋃ A \in S$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A ≼ ω) \to A \in 𝒫 S$
2		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))))$
3	2	simprbi	$⊢ S \in ⋃ ran sigAlgebra \to \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)))$
4		simpr3	$⊢ (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))) \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
5	4	exlimiv	$⊢ \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))) \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
6	3 5	syl	$⊢ S \in ⋃ ran sigAlgebra \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
7	6	3ad2ant1	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A ≼ ω) \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
8		simp3	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A ≼ ω) \to A ≼ ω$
9		breq1	$⊢ x = A \to (x ≼ ω \leftrightarrow A ≼ ω)$
10		unieq	$⊢ x = A \to ⋃ x = ⋃ A$
11	10	eleq1d	$⊢ x = A \to (⋃ x \in S \leftrightarrow ⋃ A \in S)$
12	9 11	imbi12d	$⊢ x = A \to ((x ≼ ω \to ⋃ x \in S) \leftrightarrow (A ≼ ω \to ⋃ A \in S))$
13	12	rspcv	$⊢ A \in 𝒫 S \to (\forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S) \to (A ≼ ω \to ⋃ A \in S))$
14	1 7 8 13	syl3c	$⊢ (S \in ⋃ ran sigAlgebra \land A \in 𝒫 S \land A ≼ ω) \to ⋃ A \in S$