Metamath Proof Explorer

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