Metamath Proof Explorer


Definition df-wunc

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 } )

Detailed syntax breakdown

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 } )