Theorem wuncss

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

	Ref	Expression
Assertion	wuncss	|- ( ( U e. WUni /\ A C_ U ) -> ( wUniCl ` A ) C_ U )

Proof

Step	Hyp	Ref	Expression
1		ssexg	|- ( ( A C_ U /\ U e. WUni ) -> A e. _V )
2	1	ancoms	|- ( ( U e. WUni /\ A C_ U ) -> A e. _V )
3		wuncval	|- ( A e. _V -> ( wUniCl ` A ) = |^| { u e. WUni | A C_ u } )
4	2 3	syl	|- ( ( U e. WUni /\ A C_ U ) -> ( wUniCl ` A ) = |^| { u e. WUni | A C_ u } )
5		sseq2	|- ( u = U -> ( A C_ u <-> A C_ U ) )
6	5	intminss	|- ( ( U e. WUni /\ A C_ U ) -> |^| { u e. WUni | A C_ u } C_ U )
7	4 6	eqsstrd	|- ( ( U e. WUni /\ A C_ U ) -> ( wUniCl ` A ) C_ U )