Metamath Proof Explorer

Theorem dmsigagen

Description: A sigma-algebra can be generated from any set. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion dmsigagen 
|- dom sigaGen = _V

Proof

Step Hyp Ref Expression
1 vuniex 
 |-  U. j e. _V
2 pwsiga 
 |-  ( U. j e. _V -> ~P U. j e. ( sigAlgebra ` U. j ) )
3 1 2 ax-mp 
 |-  ~P U. j e. ( sigAlgebra ` U. j )
4 pwuni 
 |-  j C_ ~P U. j
5 sseq2 
 |-  ( s = ~P U. j -> ( j C_ s <-> j C_ ~P U. j ) )
6 5 rspcev 
 |-  ( ( ~P U. j e. ( sigAlgebra ` U. j ) /\ j C_ ~P U. j ) -> E. s e. ( sigAlgebra ` U. j ) j C_ s )
7 3 4 6 mp2an 
 |-  E. s e. ( sigAlgebra ` U. j ) j C_ s
8 rabn0 
 |-  ( { s e. ( sigAlgebra ` U. j ) | j C_ s } =/= (/) <-> E. s e. ( sigAlgebra ` U. j ) j C_ s )
9 7 8 mpbir 
 |-  { s e. ( sigAlgebra ` U. j ) | j C_ s } =/= (/)
10 intex 
 |-  ( { s e. ( sigAlgebra ` U. j ) | j C_ s } =/= (/) <-> |^| { s e. ( sigAlgebra ` U. j ) | j C_ s } e. _V )
11 9 10 mpbi 
 |-  |^| { s e. ( sigAlgebra ` U. j ) | j C_ s } e. _V
12 df-sigagen 
 |-  sigaGen = ( j e. _V |-> |^| { s e. ( sigAlgebra ` U. j ) | j C_ s } )
13 11 12 dmmpti 
 |-  dom sigaGen = _V