# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to {E}\cup {F}\in {S}$

### Proof

Step Hyp Ref Expression
1 uniprg ${⊢}\left({E}\in {S}\wedge {F}\in {S}\right)\to \bigcup \left\{{E},{F}\right\}={E}\cup {F}$
2 1 eqcomd ${⊢}\left({E}\in {S}\wedge {F}\in {S}\right)\to {E}\cup {F}=\bigcup \left\{{E},{F}\right\}$
3 2 3adant1 ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to {E}\cup {F}=\bigcup \left\{{E},{F}\right\}$
4 prfi ${⊢}\left\{{E},{F}\right\}\in \mathrm{Fin}$
5 isfinite ${⊢}\left\{{E},{F}\right\}\in \mathrm{Fin}↔\left\{{E},{F}\right\}\prec \mathrm{\omega }$
6 5 biimpi ${⊢}\left\{{E},{F}\right\}\in \mathrm{Fin}\to \left\{{E},{F}\right\}\prec \mathrm{\omega }$
7 sdomdom ${⊢}\left\{{E},{F}\right\}\prec \mathrm{\omega }\to \left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }$
8 6 7 syl ${⊢}\left\{{E},{F}\right\}\in \mathrm{Fin}\to \left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }$
9 4 8 ax-mp ${⊢}\left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }$
10 9 a1i ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to \left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }$
11 prelpwi ${⊢}\left({E}\in {S}\wedge {F}\in {S}\right)\to \left\{{E},{F}\right\}\in 𝒫{S}$
12 11 3adant1 ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to \left\{{E},{F}\right\}\in 𝒫{S}$
13 issal ${⊢}{S}\in \mathrm{SAlg}\to \left({S}\in \mathrm{SAlg}↔\left(\varnothing \in {S}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {y}\in {S}\wedge \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\to \bigcup {y}\in {S}\right)\right)\right)$
14 13 ibi ${⊢}{S}\in \mathrm{SAlg}\to \left(\varnothing \in {S}\wedge \forall {y}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {y}\in {S}\wedge \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\to \bigcup {y}\in {S}\right)\right)$
15 14 simp3d ${⊢}{S}\in \mathrm{SAlg}\to \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\to \bigcup {y}\in {S}\right)$
16 15 3ad2ant1 ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\to \bigcup {y}\in {S}\right)$
17 breq1 ${⊢}{y}=\left\{{E},{F}\right\}\to \left({y}\preccurlyeq \mathrm{\omega }↔\left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }\right)$
18 unieq ${⊢}{y}=\left\{{E},{F}\right\}\to \bigcup {y}=\bigcup \left\{{E},{F}\right\}$
19 18 eleq1d ${⊢}{y}=\left\{{E},{F}\right\}\to \left(\bigcup {y}\in {S}↔\bigcup \left\{{E},{F}\right\}\in {S}\right)$
20 17 19 imbi12d ${⊢}{y}=\left\{{E},{F}\right\}\to \left(\left({y}\preccurlyeq \mathrm{\omega }\to \bigcup {y}\in {S}\right)↔\left(\left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }\to \bigcup \left\{{E},{F}\right\}\in {S}\right)\right)$
21 20 rspcva ${⊢}\left(\left\{{E},{F}\right\}\in 𝒫{S}\wedge \forall {y}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({y}\preccurlyeq \mathrm{\omega }\to \bigcup {y}\in {S}\right)\right)\to \left(\left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }\to \bigcup \left\{{E},{F}\right\}\in {S}\right)$
22 12 16 21 syl2anc ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to \left(\left\{{E},{F}\right\}\preccurlyeq \mathrm{\omega }\to \bigcup \left\{{E},{F}\right\}\in {S}\right)$
23 10 22 mpd ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to \bigcup \left\{{E},{F}\right\}\in {S}$
24 3 23 eqeltrd ${⊢}\left({S}\in \mathrm{SAlg}\wedge {E}\in {S}\wedge {F}\in {S}\right)\to {E}\cup {F}\in {S}$