Metamath Proof Explorer

Theorem salgenuni

Description: The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses salgenuni.x 
|- ( ph -> X e. V )
salgenuni.s 
|- S = ( SalGen ` X )
salgenuni.u 
|- U = U. X
Assertion salgenuni 
|- ( ph -> U. S = U )

Proof

Step Hyp Ref Expression
1 salgenuni.x 
 |-  ( ph -> X e. V )
2 salgenuni.s 
 |-  S = ( SalGen ` X )
3 salgenuni.u 
 |-  U = U. X
4 2 a1i 
 |-  ( ph -> S = ( SalGen ` X ) )
5 salgenval 
 |-  ( X e. V -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
6 1 5 syl 
 |-  ( ph -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
7 4 6 eqtrd 
 |-  ( ph -> S = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
8 7 unieqd 
 |-  ( ph -> U. S = U. |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
9 ssrab2 
 |-  { s e. SAlg | ( U. s = U. X /\ X C_ s ) } C_ SAlg
10 9 a1i 
 |-  ( ph -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } C_ SAlg )
11 salgenn0 
 |-  ( X e. V -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) )
12 1 11 syl 
 |-  ( ph -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) )
13 unieq 
 |-  ( s = t -> U. s = U. t )
14 13 eqeq1d 
 |-  ( s = t -> ( U. s = U. X <-> U. t = U. X ) )
15 sseq2 
 |-  ( s = t -> ( X C_ s <-> X C_ t ) )
16 14 15 anbi12d 
 |-  ( s = t -> ( ( U. s = U. X /\ X C_ s ) <-> ( U. t = U. X /\ X C_ t ) ) )
17 16 elrab 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> ( t e. SAlg /\ ( U. t = U. X /\ X C_ t ) ) )
18 17 biimpi 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> ( t e. SAlg /\ ( U. t = U. X /\ X C_ t ) ) )
19 18 simprld 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> U. t = U. X )
20 3 eqcomi 
 |-  U. X = U
21 20 a1i 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> U. X = U )
22 19 21 eqtrd 
 |-  ( t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> U. t = U )
23 22 adantl 
 |-  ( ( ph /\ t e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } ) -> U. t = U )
24 10 12 23 intsaluni 
 |-  ( ph -> U. |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } = U )
25 8 24 eqtrd 
 |-  ( ph -> U. S = U )