Metamath Proof Explorer

Theorem salgencl

Description: SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Assertion salgencl 
|- ( X e. V -> ( SalGen ` X ) e. SAlg )

Proof

Step Hyp Ref Expression
1 salgenval 
 |-  ( X e. V -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
2 ssrab2 
 |-  { s e. SAlg | ( U. s = U. X /\ X C_ s ) } C_ SAlg
3 2 a1i 
 |-  ( X e. V -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } C_ SAlg )
4 salgenn0 
 |-  ( X e. V -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) )
5 unieq 
 |-  ( s = t -> U. s = U. t )
6 5 eqeq1d 
 |-  ( s = t -> ( U. s = U. X <-> U. t = U. X ) )
7 sseq2 
 |-  ( s = t -> ( X C_ s <-> X C_ t ) )
8 6 7 anbi12d 
 |-  ( s = t -> ( ( U. s = U. X /\ X C_ s ) <-> ( U. t = U. X /\ X C_ t ) ) )
9 8 elrab 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> ( t e. SAlg /\ ( U. t = U. X /\ X C_ t ) ) )
10 9 biimpi 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> ( t e. SAlg /\ ( U. t = U. X /\ X C_ t ) ) )
11 10 simprld 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> U. t = U. X )
12 11 adantl 
 |-  ( ( X e. V /\ t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } ) -> U. t = U. X )
13 3 4 12 intsal 
 |-  ( X e. V -> |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } e. SAlg )
14 1 13 eqeltrd 
 |-  ( X e. V -> ( SalGen ` X ) e. SAlg )