This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressbasssg

Description: The base set of a restriction to A is a subset of A and the base set B of the original structure. (Contributed by SN, 10-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 ressbas.r 
 |-  R = ( W |`s A )
2 ressbas.b 
 |-  B = ( Base ` W )
3 1 2 ressbas 
 |-  ( A e. _V -> ( A i^i B ) = ( Base ` R ) )
4 ssid 
 |-  ( A i^i B ) C_ ( A i^i B )
5 3 4 eqsstrrdi 
 |-  ( A e. _V -> ( Base ` R ) C_ ( A i^i B ) )
6 reldmress 
 |-  Rel dom |`s
7 6 ovprc2 
 |-  ( -. A e. _V -> ( W |`s A ) = (/) )
8 1 7 eqtrid 
 |-  ( -. A e. _V -> R = (/) )
9 8 fveq2d 
 |-  ( -. A e. _V -> ( Base ` R ) = ( Base ` (/) ) )
10 base0 
 |-  (/) = ( Base ` (/) )
11 0ss 
 |-  (/) C_ ( A i^i B )
12 10 11 eqsstrri 
 |-  ( Base ` (/) ) C_ ( A i^i B )
13 9 12 eqsstrdi 
 |-  ( -. A e. _V -> ( Base ` R ) C_ ( A i^i B ) )
14 5 13 pm2.61i 
 |-  ( Base ` R ) C_ ( A i^i B )