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)

	Ref	Expression
Hypotheses	ressbas.r	|- R = ( W |`s A )
	ressbas.b	|- B = ( Base ` W )
Assertion	ressbasss	|- ( Base ` R ) C_ 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		inss2	|- ( A i^i B ) C_ B
5	3 4	eqsstrrdi	|- ( A e. _V -> ( Base ` R ) C_ B )
6		reldmress	|- Rel dom |`s
7	6	ovprc2	|- ( -. A e. _V -> ( W |`s A ) = (/) )
8	1 7	syl5eq	|- ( -. A e. _V -> R = (/) )
9	8	fveq2d	|- ( -. A e. _V -> ( Base ` R ) = ( Base ` (/) ) )
10		base0	|- (/) = ( Base ` (/) )
11		0ss	|- (/) C_ B
12	10 11	eqsstrri	|- ( Base ` (/) ) C_ B
13	9 12	eqsstrdi	|- ( -. A e. _V -> ( Base ` R ) C_ B )
14	5 13	pm2.61i	|- ( Base ` R ) C_ B