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=\mathrm{Slot}N$$
	wunstr.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunstr.s	$$⊢\phi \to S\in U$$
Assertion	wunstr	$$⊢\phi \to E\left(S\right)\in U$$

Proof

Step	Hyp	Ref	Expression
1		strfvss.e	$$⊢E=\mathrm{Slot}N$$
2		wunstr.u	$$⊢\phi \to U\in \mathrm{WUni}$$
3		wunstr.s	$$⊢\phi \to S\in U$$
4	2 3	wunrn	$$⊢\phi \to \mathrm{ran}S\in U$$
5	2 4	wununi	$$⊢\phi \to \bigcup \mathrm{ran}S\in U$$
6	1	strfvss	$$⊢E\left(S\right)\subseteq \bigcup \mathrm{ran}S$$
7	6	a1i	$$⊢\phi \to E\left(S\right)\subseteq \bigcup \mathrm{ran}S$$
8	2 5 7	wunss	$$⊢\phi \to E\left(S\right)\in U$$