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 = ( 𝑥 ∈ V ↦ ∩ { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwunm	⊢ wUniCl
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vu	⊢ 𝑢
4		cwun	⊢ WUni
5	1	cv	⊢ 𝑥
6	3	cv	⊢ 𝑢
7	5 6	wss	⊢ 𝑥 ⊆ 𝑢
8	7 3 4	crab	⊢ { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 }
9	8	cint	⊢ ∩ { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 }
10	1 2 9	cmpt	⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 } )
11	0 10	wceq	⊢ wUniCl = ( 𝑥 ∈ V ↦ ∩ { 𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢 } )