Database
TG (TARSKI-GROTHENDIECK) SET THEORY
Inaccessibles
Weak universes
df-wunc
Metamath Proof Explorer
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 ∈ V ⟼ ⋂ u ∈ WUni | x ⊆ u
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cwunm
class wUniCl
1
vx
setvar x
2
cvv
class V
3
vu
setvar u
4
cwun
class WUni
5
1
cv
setvar x
6
3
cv
setvar u
7
5 6
wss
wff x ⊆ u
8
7 3 4
crab
class u ∈ WUni | x ⊆ u
9
8
cint
class ⋂ u ∈ WUni | x ⊆ u
10
1 2 9
cmpt
class x ∈ V ⟼ ⋂ u ∈ WUni | x ⊆ u
11
0 10
wceq
wff wUniCl = x ∈ V ⟼ ⋂ u ∈ WUni | x ⊆ u