Metamath Proof Explorer


Theorem ressbasss

Description: The base set of a restriction is a subset of the base set of the original structure. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses ressbas.r R=W𝑠A
ressbas.b B=BaseW
Assertion ressbasss BaseRB

Proof

Step Hyp Ref Expression
1 ressbas.r R=W𝑠A
2 ressbas.b B=BaseW
3 1 2 ressbas AVAB=BaseR
4 inss2 ABB
5 3 4 eqsstrrdi AVBaseRB
6 reldmress Reldom𝑠
7 6 ovprc2 ¬AVW𝑠A=
8 1 7 eqtrid ¬AVR=
9 8 fveq2d ¬AVBaseR=Base
10 base0 =Base
11 0ss B
12 10 11 eqsstrri BaseB
13 9 12 eqsstrdi ¬AVBaseRB
14 5 13 pm2.61i BaseRB