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)

Step	Hyp	Ref	Expression
1		ressbas.r	$⊢ R = W ↾_{𝑠} A$
2		ressbas.b	$⊢ B = {Base}_{W}$
3	1 2	ressbas	$⊢ A \in V \to A \cap B = {Base}_{R}$
4		ssid	$⊢ A \cap B \subseteq A \cap B$
5	3 4	eqsstrrdi	$⊢ A \in V \to {Base}_{R} \subseteq A \cap B$
6		reldmress	$⊢ Rel dom ↾_{𝑠}$
7	6	ovprc2	$⊢ \neg A \in V \to W ↾_{𝑠} A = \emptyset$
8	1 7	eqtrid	$⊢ \neg A \in V \to R = \emptyset$
9	8	fveq2d	$⊢ \neg A \in V \to {Base}_{R} = {Base}_{\emptyset}$
10		base0	$⊢ \emptyset = {Base}_{\emptyset}$
11		0ss	$⊢ \emptyset \subseteq A \cap B$
12	10 11	eqsstrri	$⊢ {Base}_{\emptyset} \subseteq A \cap B$
13	9 12	eqsstrdi	$⊢ \neg A \in V \to {Base}_{R} \subseteq A \cap B$
14	5 13	pm2.61i	$⊢ {Base}_{R} \subseteq A \cap B$

Metamath Proof Explorer