Theorem ressval

Description: Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

	Ref	Expression
Hypotheses	ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
	ressbas.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	ressval	$$⊢\left(W\in X\wedge A\in Y\right)\to R=if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
2		ressbas.b	$$⊢B={\mathrm{Base}}_W$$
3		elex	$$⊢W\in X\to W\in \mathrm{V}$$
4		elex	$$⊢A\in Y\to A\in \mathrm{V}$$
5		simpl	$$⊢\left(W\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to W\in \mathrm{V}$$
6		ovex	$$⊢W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\in \mathrm{V}$$
7		ifcl	$$⊢\left(W\in \mathrm{V}\wedge W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\in \mathrm{V}\right)\to if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)\in \mathrm{V}$$
8	5 6 7	sylancl	$$⊢\left(W\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)\in \mathrm{V}$$
9		simpl	$$⊢\left(w=W\wedge a=A\right)\to w=W$$
10	9	fveq2d	$$⊢\left(w=W\wedge a=A\right)\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
11	10 2	eqtr4di	$$⊢\left(w=W\wedge a=A\right)\to {\mathrm{Base}}_w=B$$
12		simpr	$$⊢\left(w=W\wedge a=A\right)\to a=A$$
13	11 12	sseq12d	$$⊢\left(w=W\wedge a=A\right)\to \left({\mathrm{Base}}_w\subseteq a\leftrightarrow B\subseteq A\right)$$
14	12 11	ineq12d	$$⊢\left(w=W\wedge a=A\right)\to a\cap {\mathrm{Base}}_w=A\cap B$$
15	14	opeq2d	$$⊢\left(w=W\wedge a=A\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},a\cap {\mathrm{Base}}_w⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
16	9 15	oveq12d	$$⊢\left(w=W\wedge a=A\right)\to w\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},a\cap {\mathrm{Base}}_w⟩=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
17	13 9 16	ifbieq12d	$$⊢\left(w=W\wedge a=A\right)\to if\left({\mathrm{Base}}_w\subseteq a,w,w\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},a\cap {\mathrm{Base}}_w⟩\right)=if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)$$
18		df-ress	$$⊢{\upharpoonright }_{𝑠}=\left(w\in \mathrm{V},a\in \mathrm{V}⟼if\left({\mathrm{Base}}_w\subseteq a,w,w\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},a\cap {\mathrm{Base}}_w⟩\right)\right)$$
19	17 18	ovmpoga	$$⊢\left(W\in \mathrm{V}\wedge A\in \mathrm{V}\wedge if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}A=if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)$$
20	8 19	mpd3an3	$$⊢\left(W\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}A=if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)$$
21	3 4 20	syl2an	$$⊢\left(W\in X\wedge A\in Y\right)\to W{\upharpoonright }_{𝑠}A=if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)$$
22	1 21	syl5eq	$$⊢\left(W\in X\wedge A\in Y\right)\to R=if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)$$