Theorem ressid2

Description: General behavior of trivial 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	ressid2	$$⊢\left(B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W$$

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
2		ressbas.b	$$⊢B={\mathrm{Base}}_W$$
3	1 2	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)$$
4		iftrue	$$⊢B\subseteq A\to if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)=W$$
5	3 4	sylan9eqr	$$⊢\left(B\subseteq A\wedge \left(W\in X\wedge A\in Y\right)\right)\to R=W$$
6	5	3impb	$$⊢\left(B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W$$