# Metamath Proof Explorer

## Theorem salgenuni

Description: The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salgenuni.x ${⊢}{\phi }\to {X}\in {V}$
salgenuni.s ${⊢}{S}=\mathrm{SalGen}\left({X}\right)$
salgenuni.u ${⊢}{U}=\bigcup {X}$
Assertion salgenuni ${⊢}{\phi }\to \bigcup {S}={U}$

### Proof

Step Hyp Ref Expression
1 salgenuni.x ${⊢}{\phi }\to {X}\in {V}$
2 salgenuni.s ${⊢}{S}=\mathrm{SalGen}\left({X}\right)$
3 salgenuni.u ${⊢}{U}=\bigcup {X}$
4 2 a1i ${⊢}{\phi }\to {S}=\mathrm{SalGen}\left({X}\right)$
5 salgenval ${⊢}{X}\in {V}\to \mathrm{SalGen}\left({X}\right)=\bigcap \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}$
6 1 5 syl ${⊢}{\phi }\to \mathrm{SalGen}\left({X}\right)=\bigcap \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}$
7 4 6 eqtrd ${⊢}{\phi }\to {S}=\bigcap \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}$
8 7 unieqd ${⊢}{\phi }\to \bigcup {S}=\bigcup \bigcap \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}$
9 ssrab2 ${⊢}\left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\subseteq \mathrm{SAlg}$
10 9 a1i ${⊢}{\phi }\to \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\subseteq \mathrm{SAlg}$
11 salgenn0 ${⊢}{X}\in {V}\to \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\ne \varnothing$
12 1 11 syl ${⊢}{\phi }\to \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\ne \varnothing$
13 unieq ${⊢}{s}={t}\to \bigcup {s}=\bigcup {t}$
14 13 eqeq1d ${⊢}{s}={t}\to \left(\bigcup {s}=\bigcup {X}↔\bigcup {t}=\bigcup {X}\right)$
15 sseq2 ${⊢}{s}={t}\to \left({X}\subseteq {s}↔{X}\subseteq {t}\right)$
16 14 15 anbi12d ${⊢}{s}={t}\to \left(\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)↔\left(\bigcup {t}=\bigcup {X}\wedge {X}\subseteq {t}\right)\right)$
17 16 elrab ${⊢}{t}\in \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}↔\left({t}\in \mathrm{SAlg}\wedge \left(\bigcup {t}=\bigcup {X}\wedge {X}\subseteq {t}\right)\right)$
18 17 biimpi ${⊢}{t}\in \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\to \left({t}\in \mathrm{SAlg}\wedge \left(\bigcup {t}=\bigcup {X}\wedge {X}\subseteq {t}\right)\right)$
19 18 simprld ${⊢}{t}\in \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\to \bigcup {t}=\bigcup {X}$
20 3 eqcomi ${⊢}\bigcup {X}={U}$
21 20 a1i ${⊢}{t}\in \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\to \bigcup {X}={U}$
22 19 21 eqtrd ${⊢}{t}\in \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\to \bigcup {t}={U}$
23 22 adantl ${⊢}\left({\phi }\wedge {t}\in \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}\right)\to \bigcup {t}={U}$
24 10 12 23 intsaluni ${⊢}{\phi }\to \bigcup \bigcap \left\{{s}\in \mathrm{SAlg}|\left(\bigcup {s}=\bigcup {X}\wedge {X}\subseteq {s}\right)\right\}={U}$
25 8 24 eqtrd ${⊢}{\phi }\to \bigcup {S}={U}$