# Metamath Proof Explorer

## Theorem sigaclcu2

Description: A sigma-algebra is closed under countable union - indexing on NN (Contributed by Thierry Arnoux, 29-Dec-2016)

Ref Expression
Assertion sigaclcu2 ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \bigcup _{{k}\in ℕ}{A}\in {S}$

### Proof

Step Hyp Ref Expression
1 dfiun2g ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\to \bigcup _{{k}\in ℕ}{A}=\bigcup \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}$
2 1 adantl ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \bigcup _{{k}\in ℕ}{A}=\bigcup \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}$
3 simpl ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to {S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$
4 abid ${⊢}{x}\in \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}↔\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}$
5 eleq1a ${⊢}{A}\in {S}\to \left({x}={A}\to {x}\in {S}\right)$
6 5 ralimi ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {x}\in {S}\right)$
7 r19.23v ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {x}\in {S}\right)↔\left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\to {x}\in {S}\right)$
8 6 7 sylib ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\to {x}\in {S}\right)$
9 8 imp ${⊢}\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\wedge \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right)\to {x}\in {S}$
10 9 adantll ${⊢}\left(\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\wedge \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right)\to {x}\in {S}$
11 4 10 sylan2b ${⊢}\left(\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\wedge {x}\in \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\right)\to {x}\in {S}$
12 11 ralrimiva ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \forall {x}\in \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\phantom{\rule{.4em}{0ex}}{x}\in {S}$
13 nfab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}$
14 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{S}$
15 13 14 dfss3f ${⊢}\left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\subseteq {S}↔\forall {x}\in \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\phantom{\rule{.4em}{0ex}}{x}\in {S}$
16 12 15 sylibr ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\subseteq {S}$
17 elpw2g ${⊢}{S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\to \left(\left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\in 𝒫{S}↔\left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\subseteq {S}\right)$
18 17 adantr ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \left(\left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\in 𝒫{S}↔\left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\subseteq {S}\right)$
19 16 18 mpbird ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\in 𝒫{S}$
20 nnct ${⊢}ℕ\preccurlyeq \mathrm{\omega }$
21 abrexct ${⊢}ℕ\preccurlyeq \mathrm{\omega }\to \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\preccurlyeq \mathrm{\omega }$
22 20 21 mp1i ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\preccurlyeq \mathrm{\omega }$
23 sigaclcu ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\in 𝒫{S}\wedge \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\preccurlyeq \mathrm{\omega }\right)\to \bigcup \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\in {S}$
24 3 19 22 23 syl3anc ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \bigcup \left\{{x}|\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{x}={A}\right\}\in {S}$
25 2 24 eqeltrd ${⊢}\left({S}\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}\in {S}\right)\to \bigcup _{{k}\in ℕ}{A}\in {S}$