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

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
2		ressbas.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
3	1 2	ressbas	⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ 𝐵 ) = ( Base ‘ 𝑅 ) )
4		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
5	3 4	eqsstrrdi	⊢ ( 𝐴 ∈ V → ( Base ‘ 𝑅 ) ⊆ 𝐵 )
6		reldmress	⊢ Rel dom ↾s
7	6	ovprc2	⊢ ( ¬ 𝐴 ∈ V → ( 𝑊 ↾s 𝐴 ) = ∅ )
8	1 7	syl5eq	⊢ ( ¬ 𝐴 ∈ V → 𝑅 = ∅ )
9	8	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( Base ‘ 𝑅 ) = ( Base ‘ ∅ ) )
10		base0	⊢ ∅ = ( Base ‘ ∅ )
11		0ss	⊢ ∅ ⊆ 𝐵
12	10 11	eqsstrri	⊢ ( Base ‘ ∅ ) ⊆ 𝐵
13	9 12	eqsstrdi	⊢ ( ¬ 𝐴 ∈ V → ( Base ‘ 𝑅 ) ⊆ 𝐵 )
14	5 13	pm2.61i	⊢ ( Base ‘ 𝑅 ) ⊆ 𝐵