Theorem wunstr

Description: Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	strfvss.e	|- E = Slot N
	wunstr.u	|- ( ph -> U e. WUni )
	wunstr.s	|- ( ph -> S e. U )
Assertion	wunstr	|- ( ph -> ( E ` S ) e. U )

Proof

Step	Hyp	Ref	Expression
1		strfvss.e	|- E = Slot N
2		wunstr.u	|- ( ph -> U e. WUni )
3		wunstr.s	|- ( ph -> S e. U )
4	2 3	wunrn	|- ( ph -> ran S e. U )
5	2 4	wununi	|- ( ph -> U. ran S e. U )
6	1	strfvss	|- ( E ` S ) C_ U. ran S
7	6	a1i	|- ( ph -> ( E ` S ) C_ U. ran S )
8	2 5 7	wunss	|- ( ph -> ( E ` S ) e. U )