Theorem wunress

Description: Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof shortened by AV, 28-Oct-2024)

	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	1 2	basndxelwund	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in U$$
9		incom	$$⊢A\cap {\mathrm{Base}}_W={\mathrm{Base}}_W\cap A$$
10		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
11	10 1 3	wunstr	$$⊢\phi \to {\mathrm{Base}}_W\in U$$
12	1 11	wunin	$$⊢\phi \to {\mathrm{Base}}_W\cap A\in U$$
13	9 12	eqeltrid	$$⊢\phi \to A\cap {\mathrm{Base}}_W\in U$$
14	1 8 13	wunop	$$⊢\phi \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\in U$$
15	1 3 14	wunsets	$$⊢\phi \to W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\in U$$
16	3 15	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$$
17	16	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$$
18	7 17	eqeltrd	$$⊢\left(\phi \wedge A\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}A\in U$$
19	18	ex	$$⊢\phi \to \left(A\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A\in U\right)$$
20	1	wun0	$$⊢\phi \to \varnothing \in U$$
21		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
22	21	ovprc2	$$⊢\neg A\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A=\varnothing$$
23	22	eleq1d	$$⊢\neg A\in \mathrm{V}\to \left(W{\upharpoonright }_{𝑠}A\in U\leftrightarrow \varnothing \in U\right)$$
24	20 23	syl5ibrcom	$$⊢\phi \to \left(\neg A\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A\in U\right)$$
25	19 24	pm2.61d	$$⊢\phi \to W{\upharpoonright }_{𝑠}A\in U$$