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

Metamath Proof Explorer

Theorem wuncidm

Description: The weak universe closure is idempotent. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion wuncidm ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ ( wUniCl ‘ 𝐴 ) ) = ( wUniCl ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 wunccl ⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) ∈ WUni )
2 ssid ⊢ ( wUniCl ‘ 𝐴 ) ⊆ ( wUniCl ‘ 𝐴 )
3 wuncss ⊢ ( ( ( wUniCl ‘ 𝐴 ) ∈ WUni ∧ ( wUniCl ‘ 𝐴 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ( wUniCl ‘ ( wUniCl ‘ 𝐴 ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
4 1 2 3 sylancl ⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ ( wUniCl ‘ 𝐴 ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
5 wuncid ⊢ ( ( wUniCl ‘ 𝐴 ) ∈ WUni → ( wUniCl ‘ 𝐴 ) ⊆ ( wUniCl ‘ ( wUniCl ‘ 𝐴 ) ) )
6 1 5 syl ⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) ⊆ ( wUniCl ‘ ( wUniCl ‘ 𝐴 ) ) )
7 4 6 eqssd ⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ ( wUniCl ‘ 𝐴 ) ) = ( wUniCl ‘ 𝐴 ) )