Metamath Proof Explorer

Theorem sigaclcuni

Description: A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017)

Ref Expression
Hypothesis sigaclcuni.1 
|- F/_ k A
Assertion sigaclcuni 
|- ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> U_ k e. A B e. S )

Proof

Step Hyp Ref Expression
1 sigaclcuni.1 
 |-  F/_ k A
2 dfiun2g 
 |-  ( A. k e. A B e. S -> U_ k e. A B = U. { z | E. k e. A z = B } )
3 2 3ad2ant2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> U_ k e. A B = U. { z | E. k e. A z = B } )
4 simp1 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> S e. U. ran sigAlgebra )
5 r19.29 
 |-  ( ( A. k e. A B e. S /\ E. k e. A z = B ) -> E. k e. A ( B e. S /\ z = B ) )
6 simpr 
 |-  ( ( B e. S /\ z = B ) -> z = B )
7 simpl 
 |-  ( ( B e. S /\ z = B ) -> B e. S )
8 6 7 eqeltrd 
 |-  ( ( B e. S /\ z = B ) -> z e. S )
9 8 rexlimivw 
 |-  ( E. k e. A ( B e. S /\ z = B ) -> z e. S )
10 5 9 syl 
 |-  ( ( A. k e. A B e. S /\ E. k e. A z = B ) -> z e. S )
11 10 ex 
 |-  ( A. k e. A B e. S -> ( E. k e. A z = B -> z e. S ) )
12 11 abssdv 
 |-  ( A. k e. A B e. S -> { z | E. k e. A z = B } C_ S )
13 12 3ad2ant2 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> { z | E. k e. A z = B } C_ S )
14 elpw2g 
 |-  ( S e. U. ran sigAlgebra -> ( { z | E. k e. A z = B } e. ~P S <-> { z | E. k e. A z = B } C_ S ) )
15 4 14 syl 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> ( { z | E. k e. A z = B } e. ~P S <-> { z | E. k e. A z = B } C_ S ) )
16 13 15 mpbird 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> { z | E. k e. A z = B } e. ~P S )
17 1 abrexctf 
 |-  ( A ~<_ _om -> { z | E. k e. A z = B } ~<_ _om )
18 17 3ad2ant3 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> { z | E. k e. A z = B } ~<_ _om )
19 sigaclcu 
 |-  ( ( S e. U. ran sigAlgebra /\ { z | E. k e. A z = B } e. ~P S /\ { z | E. k e. A z = B } ~<_ _om ) -> U. { z | E. k e. A z = B } e. S )
20 4 16 18 19 syl3anc 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> U. { z | E. k e. A z = B } e. S )
21 3 20 eqeltrd 
 |-  ( ( S e. U. ran sigAlgebra /\ A. k e. A B e. S /\ A ~<_ _om ) -> U_ k e. A B e. S )