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 )