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

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
2		ressbas.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
3	1 2	ressbas	⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ 𝐵 ) = ( Base ‘ 𝑅 ) )
4		ssid	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 )
5	3 4	eqsstrrdi	⊢ ( 𝐴 ∈ V → ( Base ‘ 𝑅 ) ⊆ ( 𝐴 ∩ 𝐵 ) )
6		reldmress	⊢ Rel dom ↾s
7	6	ovprc2	⊢ ( ¬ 𝐴 ∈ V → ( 𝑊 ↾s 𝐴 ) = ∅ )
8	1 7	eqtrid	⊢ ( ¬ 𝐴 ∈ 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 ‘ 𝑅 ) ⊆ ( 𝐴 ∩ 𝐵 )