Metamath Proof Explorer

Definition df-salon

Description: Define the set of sigma-algebra on a given set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion df-salon 
|- SalOn = ( x e. _V |-> { s e. SAlg | U. s = x } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csalon 
 |-  SalOn
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vs 
 |-  s
4 csalg 
 |-  SAlg
5 3 cv 
 |-  s
6 5 cuni 
 |-  U. s
7 1 cv 
 |-  x
8 6 7 wceq 
 |-  U. s = x
9 8 3 4 crab 
 |-  { s e. SAlg | U. s = x }
10 1 2 9 cmpt 
 |-  ( x e. _V |-> { s e. SAlg | U. s = x } )
11 0 10 wceq 
 |-  SalOn = ( x e. _V |-> { s e. SAlg | U. s = x } )