Metamath Proof Explorer


Theorem saliuncl

Description: SAlg sigma-algebra is closed under countable indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses saliuncl.s φSSAlg
saliuncl.kct φKω
saliuncl.b φkKES
Assertion saliuncl φkKES

Proof

Step Hyp Ref Expression
1 saliuncl.s φSSAlg
2 saliuncl.kct φKω
3 saliuncl.b φkKES
4 3 ralrimiva φkKES
5 dfiun3g kKESkKE=rankKE
6 4 5 syl φkKE=rankKE
7 eqid kKE=kKE
8 7 rnmptss kKESrankKES
9 4 8 syl φrankKES
10 1 9 ssexd φrankKEV
11 elpwg rankKEVrankKE𝒫SrankKES
12 10 11 syl φrankKE𝒫SrankKES
13 9 12 mpbird φrankKE𝒫S
14 1stcrestlem KωrankKEω
15 2 14 syl φrankKEω
16 1 13 15 salunicl φrankKES
17 6 16 eqeltrd φkKES