Description: A function that maps a set x to the smallest weak universe that contains the elements of the set. (Contributed by Mario Carneiro, 2-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | df-wunc | |- wUniCl = ( x e. _V |-> |^| { u e. WUni | x C_ u } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cwunm | |- wUniCl |
|
1 | vx | |- x |
|
2 | cvv | |- _V |
|
3 | vu | |- u |
|
4 | cwun | |- WUni |
|
5 | 1 | cv | |- x |
6 | 3 | cv | |- u |
7 | 5 6 | wss | |- x C_ u |
8 | 7 3 4 | crab | |- { u e. WUni | x C_ u } |
9 | 8 | cint | |- |^| { u e. WUni | x C_ u } |
10 | 1 2 9 | cmpt | |- ( x e. _V |-> |^| { u e. WUni | x C_ u } ) |
11 | 0 10 | wceq | |- wUniCl = ( x e. _V |-> |^| { u e. WUni | x C_ u } ) |