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{\upharpoonright }_{𝑠}A$$
	ressbas.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	ressbasss	$$⊢{\mathrm{Base}}_R\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
2		ressbas.b	$$⊢B={\mathrm{Base}}_W$$
3	1 2	ressbasssg	$$⊢{\mathrm{Base}}_R\subseteq A\cap B$$
4		inss2	$$⊢A\cap B\subseteq B$$
5	3 4	sstri	$$⊢{\mathrm{Base}}_R\subseteq B$$