Theorem wunress

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

	Ref	Expression
Hypotheses	wunress.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunress.2	$$⊢\phi \to \mathrm{\omega }\in U$$
	wunress.3	$$⊢\phi \to W\in U$$
Assertion	wunress	$$⊢\phi \to W{\upharpoonright }_{𝑠}A\in U$$

Proof

Step	Hyp	Ref	Expression
1		wunress.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunress.2	$$⊢\phi \to \mathrm{\omega }\in U$$
3		wunress.3	$$⊢\phi \to W\in U$$
4		eqid	$$⊢W{\upharpoonright }_{𝑠}A=W{\upharpoonright }_{𝑠}A$$
5		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
6	4 5	ressval	$$⊢\left(W\in U\wedge A\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}A=if\left({\mathrm{Base}}_W\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\right)$$
7	3 6	sylan	$$⊢\left(\phi \wedge A\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}A=if\left({\mathrm{Base}}_W\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\right)$$
8		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
9	1 2	wunndx	$$⊢\phi \to \mathrm{ndx}\in U$$
10	8 1 9	wunstr	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$
11		incom	$$⊢A\cap {\mathrm{Base}}_W={\mathrm{Base}}_W\cap A$$
12	8 1 3	wunstr	$$⊢\phi \to {\mathrm{Base}}_W\in U$$
13	1 12	wunin	$$⊢\phi \to {\mathrm{Base}}_W\cap A\in U$$
14	11 13	eqeltrid	$$⊢\phi \to A\cap {\mathrm{Base}}_W\in U$$
15	1 10 14	wunop	$$⊢\phi \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\in U$$
16	1 3 15	wunsets	$$⊢\phi \to W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\in U$$
17	3 16	ifcld	$$⊢\phi \to if\left({\mathrm{Base}}_W\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\right)\in U$$
18	17	adantr	$$⊢\left(\phi \wedge A\in \mathrm{V}\right)\to if\left({\mathrm{Base}}_W\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\right)\in U$$
19	7 18	eqeltrd	$$⊢\left(\phi \wedge A\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}A\in U$$
20	19	ex	$$⊢\phi \to \left(A\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A\in U\right)$$
21	1	wun0	$$⊢\phi \to \varnothing \in U$$
22		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
23	22	ovprc2	$$⊢\neg A\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A=\varnothing$$
24	23	eleq1d	$$⊢\neg A\in \mathrm{V}\to \left(W{\upharpoonright }_{𝑠}A\in U\leftrightarrow \varnothing \in U\right)$$
25	21 24	syl5ibrcom	$$⊢\phi \to \left(\neg A\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A\in U\right)$$
26	20 25	pm2.61d	$$⊢\phi \to W{\upharpoonright }_{𝑠}A\in U$$