# Metamath Proof Explorer

## Theorem sigapisys

Description: All sigma-algebras are pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020)

Ref Expression
Hypothesis ispisys.p ${⊢}{P}=\left\{{s}\in 𝒫𝒫{O}|\mathrm{fi}\left({s}\right)\subseteq {s}\right\}$
Assertion sigapisys ${⊢}\mathrm{sigAlgebra}\left({O}\right)\subseteq {P}$

### Proof

Step Hyp Ref Expression
1 ispisys.p ${⊢}{P}=\left\{{s}\in 𝒫𝒫{O}|\mathrm{fi}\left({s}\right)\subseteq {s}\right\}$
2 sigasspw ${⊢}{t}\in \mathrm{sigAlgebra}\left({O}\right)\to {t}\subseteq 𝒫{O}$
3 velpw ${⊢}{t}\in 𝒫𝒫{O}↔{t}\subseteq 𝒫{O}$
4 2 3 sylibr ${⊢}{t}\in \mathrm{sigAlgebra}\left({O}\right)\to {t}\in 𝒫𝒫{O}$
5 elrnsiga ${⊢}{t}\in \mathrm{sigAlgebra}\left({O}\right)\to {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
6 5 adantr ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to {t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
7 eldifsn ${⊢}{x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)↔\left({x}\in \left(𝒫{t}\cap \mathrm{Fin}\right)\wedge {x}\ne \varnothing \right)$
8 7 biimpi ${⊢}{x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\to \left({x}\in \left(𝒫{t}\cap \mathrm{Fin}\right)\wedge {x}\ne \varnothing \right)$
9 8 adantl ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to \left({x}\in \left(𝒫{t}\cap \mathrm{Fin}\right)\wedge {x}\ne \varnothing \right)$
10 9 simpld ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to {x}\in \left(𝒫{t}\cap \mathrm{Fin}\right)$
11 10 elin1d ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to {x}\in 𝒫{t}$
12 10 elin2d ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to {x}\in \mathrm{Fin}$
13 fict ${⊢}{x}\in \mathrm{Fin}\to {x}\preccurlyeq \mathrm{\omega }$
14 12 13 syl ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to {x}\preccurlyeq \mathrm{\omega }$
15 9 simprd ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to {x}\ne \varnothing$
16 sigaclci ${⊢}\left(\left({t}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge {x}\in 𝒫{t}\right)\wedge \left({x}\preccurlyeq \mathrm{\omega }\wedge {x}\ne \varnothing \right)\right)\to \bigcap {x}\in {t}$
17 6 11 14 15 16 syl22anc ${⊢}\left({t}\in \mathrm{sigAlgebra}\left({O}\right)\wedge {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\right)\to \bigcap {x}\in {t}$
18 17 ralrimiva ${⊢}{t}\in \mathrm{sigAlgebra}\left({O}\right)\to \forall {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\bigcap {x}\in {t}$
19 4 18 jca ${⊢}{t}\in \mathrm{sigAlgebra}\left({O}\right)\to \left({t}\in 𝒫𝒫{O}\wedge \forall {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\bigcap {x}\in {t}\right)$
20 1 ispisys2 ${⊢}{t}\in {P}↔\left({t}\in 𝒫𝒫{O}\wedge \forall {x}\in \left(\left(𝒫{t}\cap \mathrm{Fin}\right)\setminus \left\{\varnothing \right\}\right)\phantom{\rule{.4em}{0ex}}\bigcap {x}\in {t}\right)$
21 19 20 sylibr ${⊢}{t}\in \mathrm{sigAlgebra}\left({O}\right)\to {t}\in {P}$
22 21 ssriv ${⊢}\mathrm{sigAlgebra}\left({O}\right)\subseteq {P}$