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 ‘ 𝐴 ) )