# Metamath Proof Explorer

## Theorem ressval2

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

Ref Expression
Hypotheses ressbas.r ${⊢}{R}={W}{↾}_{𝑠}{A}$
ressbas.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
Assertion ressval2 ${⊢}\left(¬{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}{↾}_{𝑠}{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 ${⊢}¬{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(¬{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(¬{B}\subseteq {A}\wedge {W}\in {X}\wedge {A}\in {Y}\right)\to {R}={W}\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},{A}\cap {B}⟩$