Theorem ressval2

Description: Value of nontrivial 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	ressval2	$$⊢\left(\neg B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$

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		iffalse	$$⊢\neg B\subseteq A\to if\left(B\subseteq A,W,W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
5	3 4	sylan9eqr	$$⊢\left(\neg B\subseteq A\wedge \left(W\in X\wedge A\in Y\right)\right)\to R=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
6	5	3impb	$$⊢\left(\neg B\subseteq A\wedge W\in X\wedge A\in Y\right)\to R=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$