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 φ S SAlg
saliuncl.kct φ K ω
saliuncl.b φ k K E S
Assertion saliuncl φ k K E S

Proof

Step Hyp Ref Expression
1 saliuncl.s φ S SAlg
2 saliuncl.kct φ K ω
3 saliuncl.b φ k K E S
4 nfv k φ
5 nfcv _ k S
6 nfcv _ k K
7 4 5 6 1 2 3 saliunclf φ k K E S