Metamath Proof Explorer

Theorem sigagenval

Description: Value of the generated sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion sigagenval 
|- ( A e. V -> ( sigaGen ` A ) = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )

Proof

Step Hyp Ref Expression
1 df-sigagen 
 |-  sigaGen = ( x e. _V |-> |^| { s e. ( sigAlgebra ` U. x ) | x C_ s } )
2 1 a1i 
 |-  ( A e. V -> sigaGen = ( x e. _V |-> |^| { s e. ( sigAlgebra ` U. x ) | x C_ s } ) )
3 unieq 
 |-  ( x = A -> U. x = U. A )
4 3 fveq2d 
 |-  ( x = A -> ( sigAlgebra ` U. x ) = ( sigAlgebra ` U. A ) )
5 sseq1 
 |-  ( x = A -> ( x C_ s <-> A C_ s ) )
6 4 5 rabeqbidv 
 |-  ( x = A -> { s e. ( sigAlgebra ` U. x ) | x C_ s } = { s e. ( sigAlgebra ` U. A ) | A C_ s } )
7 6 inteqd 
 |-  ( x = A -> |^| { s e. ( sigAlgebra ` U. x ) | x C_ s } = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )
8 7 adantl 
 |-  ( ( A e. V /\ x = A ) -> |^| { s e. ( sigAlgebra ` U. x ) | x C_ s } = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )
9 elex 
 |-  ( A e. V -> A e. _V )
10 uniexg 
 |-  ( A e. V -> U. A e. _V )
11 pwsiga 
 |-  ( U. A e. _V -> ~P U. A e. ( sigAlgebra ` U. A ) )
12 10 11 syl 
 |-  ( A e. V -> ~P U. A e. ( sigAlgebra ` U. A ) )
13 pwuni 
 |-  A C_ ~P U. A
14 12 13 jctir 
 |-  ( A e. V -> ( ~P U. A e. ( sigAlgebra ` U. A ) /\ A C_ ~P U. A ) )
15 sseq2 
 |-  ( s = ~P U. A -> ( A C_ s <-> A C_ ~P U. A ) )
16 15 elrab 
 |-  ( ~P U. A e. { s e. ( sigAlgebra ` U. A ) | A C_ s } <-> ( ~P U. A e. ( sigAlgebra ` U. A ) /\ A C_ ~P U. A ) )
17 14 16 sylibr 
 |-  ( A e. V -> ~P U. A e. { s e. ( sigAlgebra ` U. A ) | A C_ s } )
18 17 ne0d 
 |-  ( A e. V -> { s e. ( sigAlgebra ` U. A ) | A C_ s } =/= (/) )
19 intex 
 |-  ( { s e. ( sigAlgebra ` U. A ) | A C_ s } =/= (/) <-> |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } e. _V )
20 18 19 sylib 
 |-  ( A e. V -> |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } e. _V )
21 2 8 9 20 fvmptd 
 |-  ( A e. V -> ( sigaGen ` A ) = |^| { s e. ( sigAlgebra ` U. A ) | A C_ s } )