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

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	⊢ 𝑅 = ( 𝑊 ↾_s 𝐴 )
	ressbas.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion	ressbasss	⊢ ( Base ‘ 𝑅 ) ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	⊢ 𝑅 = ( 𝑊 ↾_s 𝐴 )
2		ressbas.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
3	1 2	ressbasssg	⊢ ( Base ‘ 𝑅 ) ⊆ ( 𝐴 ∩ 𝐵 )
4		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
5	3 4	sstri	⊢ ( Base ‘ 𝑅 ) ⊆ 𝐵