Database
TG (TARSKI-GROTHENDIECK) SET THEORY
Inaccessibles
Weak universes
wuncidm
Next ⟩
wuncval2
Metamath Proof Explorer
Ascii
Unicode
Theorem
wuncidm
Description:
The weak universe closure is idempotent.
(Contributed by
Mario Carneiro
, 2-Jan-2017)
Ref
Expression
Assertion
wuncidm
⊢
A
∈
V
→
wUniCl
⁡
wUniCl
⁡
A
=
wUniCl
⁡
A
Proof
Step
Hyp
Ref
Expression
1
wunccl
⊢
A
∈
V
→
wUniCl
⁡
A
∈
WUni
2
ssid
⊢
wUniCl
⁡
A
⊆
wUniCl
⁡
A
3
wuncss
⊢
wUniCl
⁡
A
∈
WUni
∧
wUniCl
⁡
A
⊆
wUniCl
⁡
A
→
wUniCl
⁡
wUniCl
⁡
A
⊆
wUniCl
⁡
A
4
1
2
3
sylancl
⊢
A
∈
V
→
wUniCl
⁡
wUniCl
⁡
A
⊆
wUniCl
⁡
A
5
wuncid
⊢
wUniCl
⁡
A
∈
WUni
→
wUniCl
⁡
A
⊆
wUniCl
⁡
wUniCl
⁡
A
6
1
5
syl
⊢
A
∈
V
→
wUniCl
⁡
A
⊆
wUniCl
⁡
wUniCl
⁡
A
7
4
6
eqssd
⊢
A
∈
V
→
wUniCl
⁡
wUniCl
⁡
A
=
wUniCl
⁡
A