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 )