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 𝑠 A
ressbas.b B = Base W
Assertion ressbasssg Base R A B

Proof

Step Hyp Ref Expression
1 ressbas.r R = W 𝑠 A
2 ressbas.b B = Base W
3 1 2 ressbas A V A B = Base R
4 ssid A B A B
5 3 4 eqsstrrdi A V Base R A B
6 reldmress Rel dom 𝑠
7 6 ovprc2 ¬ A V W 𝑠 A =
8 1 7 eqtrid ¬ A V R =
9 8 fveq2d ¬ A V Base R = Base
10 base0 = Base
11 0ss A B
12 10 11 eqsstrri Base A B
13 9 12 eqsstrdi ¬ A V Base R A B
14 5 13 pm2.61i Base R A B