Metamath Proof Explorer

Theorem sigagensiga

Description: A generated sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion sigagensiga 
|- ( A e. V -> ( sigaGen ` A ) e. ( sigAlgebra ` U. A ) )

Proof

Step Hyp Ref Expression
1 sigagenval 
 |-  ( A e. V -> ( sigaGen ` A ) = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )
2 fvex 
 |-  ( sigaGen ` A ) e. _V
3 1 2 eqeltrrdi 
 |-  ( A e. V -> |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } e. _V )
4 intex 
 |-  ( { s e. ( sigAlgebra ` U. A ) | A C_ s } =/= (/) <-> |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } e. _V )
5 3 4 sylibr 
 |-  ( A e. V -> { s e. ( sigAlgebra ` U. A ) | A C_ s } =/= (/) )
6 ssrab2 
 |-  { s e. ( sigAlgebra ` U. A ) | A C_ s } C_ ( sigAlgebra ` U. A )
7 6 a1i 
 |-  ( A e. V -> { s e. ( sigAlgebra ` U. A ) | A C_ s } C_ ( sigAlgebra ` U. A ) )
8 fvex 
 |-  ( sigAlgebra ` U. A ) e. _V
9 8 elpw2 
 |-  ( { s e. ( sigAlgebra ` U. A ) | A C_ s } e. ~P ( sigAlgebra ` U. A ) <-> { s e. ( sigAlgebra ` U. A ) | A C_ s } C_ ( sigAlgebra ` U. A ) )
10 7 9 sylibr 
 |-  ( A e. V -> { s e. ( sigAlgebra ` U. A ) | A C_ s } e. ~P ( sigAlgebra ` U. A ) )
11 insiga 
 |-  ( ( { s e. ( sigAlgebra ` U. A ) | A C_ s } =/= (/) /\ { s e. ( sigAlgebra ` U. A ) | A C_ s } e. ~P ( sigAlgebra ` U. A ) ) -> |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } e. ( sigAlgebra ` U. A ) )
12 5 10 11 syl2anc 
 |-  ( A e. V -> |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } e. ( sigAlgebra ` U. A ) )
13 1 12 eqeltrd 
 |-  ( A e. V -> ( sigaGen ` A ) e. ( sigAlgebra ` U. A ) )