This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑥 ∈ 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 ∣ 𝑥 ⊆ 𝑢 } )