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