Metamath Proof Explorer

Theorem unelsiga

Description: A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016)

		Ref	Expression
	Assertion	unelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to A \cup B \in S$

Proof

Step	Hyp	Ref	Expression
1		uniprg	$⊢ (A \in S \land B \in S) \to ⋃ \{A, B\} = A \cup B$
2	1	3adant1	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to ⋃ \{A, B\} = A \cup B$
3		isrnsigau	$⊢ S \in ⋃ ran sigAlgebra \to (S \subseteq 𝒫 ⋃ S \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
4	3	simprd	$⊢ S \in ⋃ ran sigAlgebra \to (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
5	4	simp3d	$⊢ S \in ⋃ ran sigAlgebra \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
6	5	3ad2ant1	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
7		prct	$⊢ (A \in S \land B \in S) \to \{A, B\} ≼ ω$
8	7	3adant1	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to \{A, B\} ≼ ω$
9		prelpwi	$⊢ (A \in S \land B \in S) \to \{A, B\} \in 𝒫 S$
10		breq1	$⊢ x = \{A, B\} \to (x ≼ ω \leftrightarrow \{A, B\} ≼ ω)$
11		unieq	$⊢ x = \{A, B\} \to ⋃ x = ⋃ \{A, B\}$
12	11	eleq1d	$⊢ x = \{A, B\} \to (⋃ x \in S \leftrightarrow ⋃ \{A, B\} \in S)$
13	10 12	imbi12d	$⊢ x = \{A, B\} \to ((x ≼ ω \to ⋃ x \in S) \leftrightarrow (\{A, B\} ≼ ω \to ⋃ \{A, B\} \in S))$
14	13	rspcv	$⊢ \{A, B\} \in 𝒫 S \to (\forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S) \to (\{A, B\} ≼ ω \to ⋃ \{A, B\} \in S))$
15	9 14	syl	$⊢ (A \in S \land B \in S) \to (\forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S) \to (\{A, B\} ≼ ω \to ⋃ \{A, B\} \in S))$
16	15	3adant1	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to (\forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S) \to (\{A, B\} ≼ ω \to ⋃ \{A, B\} \in S))$
17	6 8 16	mp2d	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to ⋃ \{A, B\} \in S$
18	2 17	eqeltrrd	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S \land B \in S) \to A \cup B \in S$