Metamath Proof Explorer

Theorem wuncidm

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

Ref Expression
Assertion wuncidm 
|- ( A e. V -> ( wUniCl ` ( wUniCl ` A ) ) = ( wUniCl ` A ) )

Proof

Step Hyp Ref Expression
1 wunccl 
 |-  ( A e. V -> ( wUniCl ` A ) e. WUni )
2 ssid 
 |-  ( wUniCl ` A ) C_ ( wUniCl ` A )
3 wuncss 
 |-  ( ( ( wUniCl ` A ) e. WUni /\ ( wUniCl ` A ) C_ ( wUniCl ` A ) ) -> ( wUniCl ` ( wUniCl ` A ) ) C_ ( wUniCl ` A ) )
4 1 2 3 sylancl 
 |-  ( A e. V -> ( wUniCl ` ( wUniCl ` A ) ) C_ ( wUniCl ` A ) )
5 wuncid 
 |-  ( ( wUniCl ` A ) e. WUni -> ( wUniCl ` A ) C_ ( wUniCl ` ( wUniCl ` A ) ) )
6 1 5 syl 
 |-  ( A e. V -> ( wUniCl ` A ) C_ ( wUniCl ` ( wUniCl ` A ) ) )
7 4 6 eqssd 
 |-  ( A e. V -> ( wUniCl ` ( wUniCl ` A ) ) = ( wUniCl ` A ) )