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

Metamath Proof Explorer

Theorem wunccl

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

Ref Expression
Assertion wunccl 
|- ( A e. V -> ( wUniCl ` A ) e. WUni )

Proof

Step Hyp Ref Expression
1 wuncval 
 |-  ( A e. V -> ( wUniCl ` A ) = |^| { u e. WUni | A C_ u } )
2 ssrab2 
 |-  { u e. WUni | A C_ u } C_ WUni
3 wunex 
 |-  ( A e. V -> E. u e. WUni A C_ u )
4 rabn0 
 |-  ( { u e. WUni | A C_ u } =/= (/) <-> E. u e. WUni A C_ u )
5 3 4 sylibr 
 |-  ( A e. V -> { u e. WUni | A C_ u } =/= (/) )
6 intwun 
 |-  ( ( { u e. WUni | A C_ u } C_ WUni /\ { u e. WUni | A C_ u } =/= (/) ) -> |^| { u e. WUni | A C_ u } e. WUni )
7 2 5 6 sylancr 
 |-  ( A e. V -> |^| { u e. WUni | A C_ u } e. WUni )
8 1 7 eqeltrd 
 |-  ( A e. V -> ( wUniCl ` A ) e. WUni )