Theorem wunressOLD

Description: Obsolete version of wunress as of 28-Oct-2024. Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

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