# Metamath Proof Explorer

## Theorem issgon

Description: Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016) (Revised by Thierry Arnoux, 23-Oct-2016)

Ref Expression
Assertion issgon ${⊢}{S}\in \mathrm{sigAlgebra}\left({O}\right)↔\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {O}=\bigcup {S}\right)$

### Proof

Step Hyp Ref Expression
1 fvssunirn ${⊢}\mathrm{sigAlgebra}\left({O}\right)\subseteq \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
2 1 sseli ${⊢}{S}\in \mathrm{sigAlgebra}\left({O}\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
3 elex ${⊢}{S}\in \mathrm{sigAlgebra}\left({O}\right)\to {S}\in \mathrm{V}$
4 issiga ${⊢}{S}\in \mathrm{V}\to \left({S}\in \mathrm{sigAlgebra}\left({O}\right)↔\left({S}\subseteq 𝒫{O}\wedge \left({O}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)$
5 elpwuni ${⊢}{O}\in {S}\to \left({S}\subseteq 𝒫{O}↔\bigcup {S}={O}\right)$
6 5 biimpa ${⊢}\left({O}\in {S}\wedge {S}\subseteq 𝒫{O}\right)\to \bigcup {S}={O}$
7 ancom ${⊢}\left({S}\subseteq 𝒫{O}\wedge {O}\in {S}\right)↔\left({O}\in {S}\wedge {S}\subseteq 𝒫{O}\right)$
8 eqcom ${⊢}{O}=\bigcup {S}↔\bigcup {S}={O}$
9 6 7 8 3imtr4i ${⊢}\left({S}\subseteq 𝒫{O}\wedge {O}\in {S}\right)\to {O}=\bigcup {S}$
10 9 3ad2antr1 ${⊢}\left({S}\subseteq 𝒫{O}\wedge \left({O}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\to {O}=\bigcup {S}$
11 4 10 syl6bi ${⊢}{S}\in \mathrm{V}\to \left({S}\in \mathrm{sigAlgebra}\left({O}\right)\to {O}=\bigcup {S}\right)$
12 3 11 mpcom ${⊢}{S}\in \mathrm{sigAlgebra}\left({O}\right)\to {O}=\bigcup {S}$
13 2 12 jca ${⊢}{S}\in \mathrm{sigAlgebra}\left({O}\right)\to \left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {O}=\bigcup {S}\right)$
14 elex ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to {S}\in \mathrm{V}$
15 isrnsiga ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}↔\left({S}\in \mathrm{V}\wedge \exists {o}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)$
16 15 simprbi ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \exists {o}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
17 elpwuni ${⊢}{o}\in {S}\to \left({S}\subseteq 𝒫{o}↔\bigcup {S}={o}\right)$
18 17 biimpa ${⊢}\left({o}\in {S}\wedge {S}\subseteq 𝒫{o}\right)\to \bigcup {S}={o}$
19 ancom ${⊢}\left({S}\subseteq 𝒫{o}\wedge {o}\in {S}\right)↔\left({o}\in {S}\wedge {S}\subseteq 𝒫{o}\right)$
20 eqcom ${⊢}{o}=\bigcup {S}↔\bigcup {S}={o}$
21 18 19 20 3imtr4i ${⊢}\left({S}\subseteq 𝒫{o}\wedge {o}\in {S}\right)\to {o}=\bigcup {S}$
22 21 3ad2antr1 ${⊢}\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\to {o}=\bigcup {S}$
23 pweq ${⊢}{o}=\bigcup {S}\to 𝒫{o}=𝒫\bigcup {S}$
24 23 sseq2d ${⊢}{o}=\bigcup {S}\to \left({S}\subseteq 𝒫{o}↔{S}\subseteq 𝒫\bigcup {S}\right)$
25 eleq1 ${⊢}{o}=\bigcup {S}\to \left({o}\in {S}↔\bigcup {S}\in {S}\right)$
26 difeq1 ${⊢}{o}=\bigcup {S}\to {o}\setminus {x}=\bigcup {S}\setminus {x}$
27 26 eleq1d ${⊢}{o}=\bigcup {S}\to \left({o}\setminus {x}\in {S}↔\bigcup {S}\setminus {x}\in {S}\right)$
28 27 ralbidv ${⊢}{o}=\bigcup {S}\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\right)$
29 25 28 3anbi12d ${⊢}{o}=\bigcup {S}\to \left(\left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)↔\left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
30 24 29 anbi12d ${⊢}{o}=\bigcup {S}\to \left(\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)↔\left({S}\subseteq 𝒫\bigcup {S}\wedge \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)$
31 22 30 syl ${⊢}\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\to \left(\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)↔\left({S}\subseteq 𝒫\bigcup {S}\wedge \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)$
32 31 ibi ${⊢}\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\to \left({S}\subseteq 𝒫\bigcup {S}\wedge \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
33 32 exlimiv ${⊢}\exists {o}\phantom{\rule{.4em}{0ex}}\left({S}\subseteq 𝒫{o}\wedge \left({o}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\to \left({S}\subseteq 𝒫\bigcup {S}\wedge \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
34 16 33 syl ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left({S}\subseteq 𝒫\bigcup {S}\wedge \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
35 34 simprd ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)$
36 14 35 jca ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left({S}\in \mathrm{V}\wedge \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
37 eleq1 ${⊢}{O}=\bigcup {S}\to \left({O}\in {S}↔\bigcup {S}\in {S}\right)$
38 difeq1 ${⊢}{O}=\bigcup {S}\to {O}\setminus {x}=\bigcup {S}\setminus {x}$
39 38 eleq1d ${⊢}{O}=\bigcup {S}\to \left({O}\setminus {x}\in {S}↔\bigcup {S}\setminus {x}\in {S}\right)$
40 39 ralbidv ${⊢}{O}=\bigcup {S}\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\right)$
41 37 40 3anbi12d ${⊢}{O}=\bigcup {S}\to \left(\left({O}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)↔\left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
42 41 biimprd ${⊢}{O}=\bigcup {S}\to \left(\left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\to \left({O}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)$
43 pwuni ${⊢}{S}\subseteq 𝒫\bigcup {S}$
44 pweq ${⊢}{O}=\bigcup {S}\to 𝒫{O}=𝒫\bigcup {S}$
45 43 44 sseqtrrid ${⊢}{O}=\bigcup {S}\to {S}\subseteq 𝒫{O}$
46 42 45 jctild ${⊢}{O}=\bigcup {S}\to \left(\left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\to \left({S}\subseteq 𝒫{O}\wedge \left({O}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)$
47 46 anim2d ${⊢}{O}=\bigcup {S}\to \left(\left({S}\in \mathrm{V}\wedge \left(\bigcup {S}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\bigcup {S}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\to \left({S}\in \mathrm{V}\wedge \left({S}\subseteq 𝒫{O}\wedge \left({O}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)\right)$
48 4 biimpar ${⊢}\left({S}\in \mathrm{V}\wedge \left({S}\subseteq 𝒫{O}\wedge \left({O}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {S}\wedge \forall {x}\in 𝒫{S}\phantom{\rule{.4em}{0ex}}\left({x}\preccurlyeq \mathrm{\omega }\to \bigcup {x}\in {S}\right)\right)\right)\right)\to {S}\in \mathrm{sigAlgebra}\left({O}\right)$
49 36 47 48 syl56 ${⊢}{O}=\bigcup {S}\to \left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to {S}\in \mathrm{sigAlgebra}\left({O}\right)\right)$
50 49 impcom ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {O}=\bigcup {S}\right)\to {S}\in \mathrm{sigAlgebra}\left({O}\right)$
51 13 50 impbii ${⊢}{S}\in \mathrm{sigAlgebra}\left({O}\right)↔\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {O}=\bigcup {S}\right)$