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	$$⊢\mathrm{wUniCl}=\left(x\in \mathrm{V}⟼\bigcap \left\{u\in \mathrm{WUni}|x\subseteq u\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwunm	$$class\mathrm{wUniCl}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vu	$$setvaru$$
4		cwun	$$class\mathrm{WUni}$$
5	1	cv	$$setvarx$$
6	3	cv	$$setvaru$$
7	5 6	wss	$$wffx\subseteq u$$
8	7 3 4	crab	$$class\left\{u\in \mathrm{WUni}|x\subseteq u\right\}$$
9	8	cint	$$class\bigcap \left\{u\in \mathrm{WUni}|x\subseteq u\right\}$$
10	1 2 9	cmpt	$$class\left(x\in \mathrm{V}⟼\bigcap \left\{u\in \mathrm{WUni}|x\subseteq u\right\}\right)$$
11	0 10	wceq	$$wff\mathrm{wUniCl}=\left(x\in \mathrm{V}⟼\bigcap \left\{u\in \mathrm{WUni}|x\subseteq u\right\}\right)$$