Metamath Proof Explorer

Theorem salgenval

Description: The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Assertion salgenval 
|- ( X e. V -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )

Proof

Step Hyp Ref Expression
1 df-salgen 
 |-  SalGen = ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } )
2 1 a1i 
 |-  ( X e. V -> SalGen = ( x e. _V |-> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } ) )
3 unieq 
 |-  ( x = X -> U. x = U. X )
4 3 eqeq2d 
 |-  ( x = X -> ( U. s = U. x <-> U. s = U. X ) )
5 sseq1 
 |-  ( x = X -> ( x C_ s <-> X C_ s ) )
6 4 5 anbi12d 
 |-  ( x = X -> ( ( U. s = U. x /\ x C_ s ) <-> ( U. s = U. X /\ X C_ s ) ) )
7 6 rabbidv 
 |-  ( x = X -> { s e. SAlg | ( U. s = U. x /\ x C_ s ) } = { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
8 7 inteqd 
 |-  ( x = X -> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
9 8 adantl 
 |-  ( ( X e. V /\ x = X ) -> |^| { s e. SAlg | ( U. s = U. x /\ x C_ s ) } = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
10 elex 
 |-  ( X e. V -> X e. _V )
11 uniexg 
 |-  ( X e. V -> U. X e. _V )
12 pwsal 
 |-  ( U. X e. _V -> ~P U. X e. SAlg )
13 11 12 syl 
 |-  ( X e. V -> ~P U. X e. SAlg )
14 unipw 
 |-  U. ~P U. X = U. X
15 14 a1i 
 |-  ( X e. V -> U. ~P U. X = U. X )
16 pwuni 
 |-  X C_ ~P U. X
17 16 a1i 
 |-  ( X e. V -> X C_ ~P U. X )
18 13 15 17 jca32 
 |-  ( X e. V -> ( ~P U. X e. SAlg /\ ( U. ~P U. X = U. X /\ X C_ ~P U. X ) ) )
19 unieq 
 |-  ( s = ~P U. X -> U. s = U. ~P U. X )
20 19 eqeq1d 
 |-  ( s = ~P U. X -> ( U. s = U. X <-> U. ~P U. X = U. X ) )
21 sseq2 
 |-  ( s = ~P U. X -> ( X C_ s <-> X C_ ~P U. X ) )
22 20 21 anbi12d 
 |-  ( s = ~P U. X -> ( ( U. s = U. X /\ X C_ s ) <-> ( U. ~P U. X = U. X /\ X C_ ~P U. X ) ) )
23 22 elrab 
 |-  ( ~P U. X e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } <-> ( ~P U. X e. SAlg /\ ( U. ~P U. X = U. X /\ X C_ ~P U. X ) ) )
24 18 23 sylibr 
 |-  ( X e. V -> ~P U. X e. { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )
25 24 ne0d 
 |-  ( X e. V -> { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) )
26 intex 
 |-  ( { s e. SAlg | ( U. s = U. X /\ X C_ s ) } =/= (/) <-> |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } e. _V )
27 25 26 sylib 
 |-  ( X e. V -> |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } e. _V )
28 2 9 10 27 fvmptd 
 |-  ( X e. V -> ( SalGen ` X ) = |^| { s e. SAlg | ( U. s = U. X /\ X C_ s ) } )