Definition df-wunc 10390

Description: A function that maps a set 𝑥 to the smallest weak universe that contains the elements of the set. (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-wunc	⊢ wUniCl = (𝑥 ∈ V ↦ ∩ {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢})

Distinct variable group:   𝑥,𝑢

Detailed syntax breakdown of Definition df-wunc

Step	Hyp	Ref	Expression
1		cwunm 10388	. 2 class wUniCl
2		vx	. . 3 setvar 𝑥
3		cvv 3422	. . 3 class V
4	2	cv 1538	. . . . . 6 class 𝑥
5		vu	. . . . . . 7 setvar 𝑢
6	5	cv 1538	. . . . . 6 class 𝑢
7	4, 6	wss 3883	. . . . 5 wff 𝑥 ⊆ 𝑢
8		cwun 10387	. . . . 5 class WUni
9	7, 5, 8	crab 3067	. . . 4 class {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢}
10	9	cint 4876	. . 3 class ∩ {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢}
11	2, 3, 10	cmpt 5153	. 2 class (𝑥 ∈ V ↦ ∩ {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢})
12	1, 11	wceq 1539	1 wff wUniCl = (𝑥 ∈ V ↦ ∩ {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢})

This definition is referenced by:  wuncval  10429