Theorem wunsets

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

	Ref	Expression
Hypotheses	wunsets.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunsets.2	$$⊢\phi \to S\in U$$
	wunsets.3	$$⊢\phi \to A\in U$$
Assertion	wunsets	$$⊢\phi \to S\mathrm{sSet}A\in U$$

Proof

Step	Hyp	Ref	Expression
1		wunsets.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunsets.2	$$⊢\phi \to S\in U$$
3		wunsets.3	$$⊢\phi \to A\in U$$
4		setsvalg	$$⊢\left(S\in U\wedge A\in U\right)\to S\mathrm{sSet}A=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{A\right\}\right)}\right)\cup \left\{A\right\}$$
5	2 3 4	syl2anc	$$⊢\phi \to S\mathrm{sSet}A=\left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{A\right\}\right)}\right)\cup \left\{A\right\}$$
6	1 2	wunres	$$⊢\phi \to {S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{A\right\}\right)}\in U$$
7	1 3	wunsn	$$⊢\phi \to \left\{A\right\}\in U$$
8	1 6 7	wunun	$$⊢\phi \to \left({S\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{A\right\}\right)}\right)\cup \left\{A\right\}\in U$$
9	5 8	eqeltrd	$$⊢\phi \to S\mathrm{sSet}A\in U$$