Metamath Proof Explorer

Theorem issalgend

Description: One side of dfsalgen2 . If a sigma-algebra on U. X includes X and it is included in all the sigma-algebras with such two properties, then it is the sigma-algebra generated by X . (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses issalgend.x 
|- ( ph -> X e. V )
issalgend.s 
|- ( ph -> S e. SAlg )
issalgend.u 
|- ( ph -> U. S = U. X )
issalgend.i 
|- ( ph -> X C_ S )
issalgend.a 
|- ( ( ph /\ ( y e. SAlg /\ U. y = U. X /\ X C_ y ) ) -> S C_ y )
Assertion issalgend 
|- ( ph -> ( SalGen ` X ) = S )

Proof

Step Hyp Ref Expression
1 issalgend.x 
 |-  ( ph -> X e. V )
2 issalgend.s 
 |-  ( ph -> S e. SAlg )
3 issalgend.u 
 |-  ( ph -> U. S = U. X )
4 issalgend.i 
 |-  ( ph -> X C_ S )
5 issalgend.a 
 |-  ( ( ph /\ ( y e. SAlg /\ U. y = U. X /\ X C_ y ) ) -> S C_ y )
6 eqid 
 |-  ( SalGen ` X ) = ( SalGen ` X )
7 1 6 2 4 3 salgenss 
 |-  ( ph -> ( SalGen ` X ) C_ S )
8 simpl 
 |-  ( ( ph /\ y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } ) -> ph )
9 elrabi 
 |-  ( y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> y e. SAlg )
10 9 adantl 
 |-  ( ( ph /\ y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } ) -> y e. SAlg )
11 unieq 
 |-  ( s = y -> U. s = U. y )
12 11 eqeq1d 
 |-  ( s = y -> ( U. s = U. X <-> U. y = U. X ) )
13 sseq2 
 |-  ( s = y -> ( X C_ s <-> X C_ y ) )
14 12 13 anbi12d 
 |-  ( s = y -> ( ( U. s = U. X /\ X C_ s ) <-> ( U. y = U. X /\ X C_ y ) ) )
15 14 elrab 
 |-  ( y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> ( y e. SAlg /\ ( U. y = U. X /\ X C_ y ) ) )
16 15 biimpi 
 |-  ( y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> ( y e. SAlg /\ ( U. y = U. X /\ X C_ y ) ) )
17 16 simprld 
 |-  ( y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> U. y = U. X )
18 17 adantl 
 |-  ( ( ph /\ y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } ) -> U. y = U. X )
19 16 simprrd 
 |-  ( y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } -> X C_ y )
20 19 adantl 
 |-  ( ( ph /\ y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } ) -> X C_ y )
21 8 10 18 20 5 syl13anc 
 |-  ( ( ph /\ y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } ) -> S C_ y )
22 21 ralrimiva 
 |-  ( ph -> A. y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } S C_ y )
23 ssint 
 |-  ( S C_ |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> A. y e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } S C_ y )
24 22 23 sylibr 
 |-  ( ph -> S C_ |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
25 salgenval 
 |-  ( X e. V -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
26 1 25 syl 
 |-  ( ph -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
27 24 26 sseqtrrd 
 |-  ( ph -> S C_ ( SalGen ` X ) )
28 7 27 eqssd 
 |-  ( ph -> ( SalGen ` X ) = S )