saluncl

Description: The union of two sets in a sigma-algebra is in the sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	saluncl	$⊢ (S \in SAlg \land E \in S \land F \in S) \to E \cup F \in S$

Proof

Step	Hyp	Ref	Expression
1		uniprg	$⊢ (E \in S \land F \in S) \to ⋃ \{E, F\} = E \cup F$
2	1	eqcomd	$⊢ (E \in S \land F \in S) \to E \cup F = ⋃ \{E, F\}$
3	2	3adant1	$⊢ (S \in SAlg \land E \in S \land F \in S) \to E \cup F = ⋃ \{E, F\}$
4		prfi	$⊢ \{E, F\} \in Fin$
5		isfinite	$⊢ \{E, F\} \in Fin \leftrightarrow \{E, F\} ≺ ω$
6	5	biimpi	$⊢ \{E, F\} \in Fin \to \{E, F\} ≺ ω$
7		sdomdom	$⊢ \{E, F\} ≺ ω \to \{E, F\} ≼ ω$
8	6 7	syl	$⊢ \{E, F\} \in Fin \to \{E, F\} ≼ ω$
9	4 8	ax-mp	$⊢ \{E, F\} ≼ ω$
10	9	a1i	$⊢ (S \in SAlg \land E \in S \land F \in S) \to \{E, F\} ≼ ω$
11		prelpwi	$⊢ (E \in S \land F \in S) \to \{E, F\} \in 𝒫 S$
12	11	3adant1	$⊢ (S \in SAlg \land E \in S \land F \in S) \to \{E, F\} \in 𝒫 S$
13		issal	$⊢ S \in SAlg \to (S \in SAlg \leftrightarrow (\emptyset \in S \land \forall y \in S ⋃ S ∖ y \in S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)))$
14	13	ibi	$⊢ S \in SAlg \to (\emptyset \in S \land \forall y \in S ⋃ S ∖ y \in S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S))$
15	14	simp3d	$⊢ S \in SAlg \to \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)$
16	15	3ad2ant1	$⊢ (S \in SAlg \land E \in S \land F \in S) \to \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)$
17		breq1	$⊢ y = \{E, F\} \to (y ≼ ω \leftrightarrow \{E, F\} ≼ ω)$
18		unieq	$⊢ y = \{E, F\} \to ⋃ y = ⋃ \{E, F\}$
19	18	eleq1d	$⊢ y = \{E, F\} \to (⋃ y \in S \leftrightarrow ⋃ \{E, F\} \in S)$
20	17 19	imbi12d	$⊢ y = \{E, F\} \to ((y ≼ ω \to ⋃ y \in S) \leftrightarrow (\{E, F\} ≼ ω \to ⋃ \{E, F\} \in S))$
21	20	rspcva	$⊢ (\{E, F\} \in 𝒫 S \land \forall y \in 𝒫 S (y ≼ ω \to ⋃ y \in S)) \to (\{E, F\} ≼ ω \to ⋃ \{E, F\} \in S)$
22	12 16 21	syl2anc	$⊢ (S \in SAlg \land E \in S \land F \in S) \to (\{E, F\} ≼ ω \to ⋃ \{E, F\} \in S)$
23	10 22	mpd	$⊢ (S \in SAlg \land E \in S \land F \in S) \to ⋃ \{E, F\} \in S$
24	3 23	eqeltrd	$⊢ (S \in SAlg \land E \in S \land F \in S) \to E \cup F \in S$

Metamath Proof Explorer

Theorem saluncl

Proof