Metamath Proof Explorer

Theorem elsigagen2

Description: Any countable union of elements of a set is also in the sigma-algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017)

Ref Expression
Assertion elsigagen2 
|- ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> U. B e. ( sigaGen ` A ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> A e. V )
2 1 sgsiga 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> ( sigaGen ` A ) e. U. ran sigAlgebra )
3 sssigagen 
 |-  ( A e. V -> A C_ ( sigaGen ` A ) )
4 sspw 
 |-  ( A C_ ( sigaGen ` A ) -> ~P A C_ ~P ( sigaGen ` A ) )
5 1 3 4 3syl 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> ~P A C_ ~P ( sigaGen ` A ) )
6 simp2 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> B C_ A )
7 simp3 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> B ~<_ _om )
8 ctex 
 |-  ( B ~<_ _om -> B e. _V )
9 elpwg 
 |-  ( B e. _V -> ( B e. ~P A <-> B C_ A ) )
10 7 8 9 3syl 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> ( B e. ~P A <-> B C_ A ) )
11 6 10 mpbird 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> B e. ~P A )
12 5 11 sseldd 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> B e. ~P ( sigaGen ` A ) )
13 sigaclcu 
 |-  ( ( ( sigaGen ` A ) e. U. ran sigAlgebra /\ B e. ~P ( sigaGen ` A ) /\ B ~<_ _om ) -> U. B e. ( sigaGen ` A ) )
14 2 12 7 13 syl3anc 
 |-  ( ( A e. V /\ B C_ A /\ B ~<_ _om ) -> U. B e. ( sigaGen ` A ) )