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) (Proof shortened by SN, 25-Feb-2025)

Ref Expression
Hypotheses ressbas.r
|- R = ( W |`s A )
ressbas.b
|- B = ( Base ` W )
Assertion ressbasss
|- ( Base ` R ) C_ B

Proof

Step Hyp Ref Expression
1 ressbas.r
 |-  R = ( W |`s A )
2 ressbas.b
 |-  B = ( Base ` W )
3 1 2 ressbasssg
 |-  ( Base ` R ) C_ ( A i^i B )
4 inss2
 |-  ( A i^i B ) C_ B
5 3 4 sstri
 |-  ( Base ` R ) C_ B