# Metamath Proof Explorer

## Theorem sigaval

Description: The set of sigma-algebra with a given base set. (Contributed by Thierry Arnoux, 23-Sep-2016)

Ref Expression
Assertion sigaval ${⊢}{O}\in \mathrm{V}\to \mathrm{sigAlgebra}\left({O}\right)=\left\{{s}|\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\}$

### Proof

Step Hyp Ref Expression
1 df-rab ${⊢}\left\{{s}\in 𝒫𝒫{O}|\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}|\left({s}\in 𝒫𝒫{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\}$
2 velpw ${⊢}{s}\in 𝒫𝒫{O}↔{s}\subseteq 𝒫{O}$
3 2 anbi1i ${⊢}\left({s}\in 𝒫𝒫{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 𝒫{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)$
4 3 abbii ${⊢}\left\{{s}|\left({s}\in 𝒫𝒫{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\}=\left\{{s}|\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 1 4 eqtri ${⊢}\left\{{s}\in 𝒫𝒫{O}|\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}|\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\}$
6 pwexg ${⊢}{O}\in \mathrm{V}\to 𝒫{O}\in \mathrm{V}$
7 pwexg ${⊢}𝒫{O}\in \mathrm{V}\to 𝒫𝒫{O}\in \mathrm{V}$
8 rabexg ${⊢}𝒫𝒫{O}\in \mathrm{V}\to \left\{{s}\in 𝒫𝒫{O}|\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\}\in \mathrm{V}$
9 6 7 8 3syl ${⊢}{O}\in \mathrm{V}\to \left\{{s}\in 𝒫𝒫{O}|\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\}\in \mathrm{V}$
10 5 9 eqeltrrid ${⊢}{O}\in \mathrm{V}\to \left\{{s}|\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\}\in \mathrm{V}$
11 pweq ${⊢}{o}={O}\to 𝒫{o}=𝒫{O}$
12 11 sseq2d ${⊢}{o}={O}\to \left({s}\subseteq 𝒫{o}↔{s}\subseteq 𝒫{O}\right)$
13 eleq1 ${⊢}{o}={O}\to \left({o}\in {s}↔{O}\in {s}\right)$
14 difeq1 ${⊢}{o}={O}\to {o}\setminus {x}={O}\setminus {x}$
15 14 eleq1d ${⊢}{o}={O}\to \left({o}\setminus {x}\in {s}↔{O}\setminus {x}\in {s}\right)$
16 15 ralbidv ${⊢}{o}={O}\to \left(\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}{o}\setminus {x}\in {s}↔\forall {x}\in {s}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {s}\right)$
17 13 16 3anbi12d ${⊢}{o}={O}\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({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)$
18 12 17 anbi12d ${⊢}{o}={O}\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 𝒫{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)$
19 18 abbidv ${⊢}{o}={O}\to \left\{{s}|\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\}=\left\{{s}|\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\}$
20 df-siga ${⊢}\mathrm{sigAlgebra}=\left({o}\in \mathrm{V}⟼\left\{{s}|\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)$
21 19 20 fvmptg ${⊢}\left({O}\in \mathrm{V}\wedge \left\{{s}|\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\}\in \mathrm{V}\right)\to \mathrm{sigAlgebra}\left({O}\right)=\left\{{s}|\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\}$
22 10 21 mpdan ${⊢}{O}\in \mathrm{V}\to \mathrm{sigAlgebra}\left({O}\right)=\left\{{s}|\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\}$