This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ressbasssOLD

Description: Obsolete version of ressbas as of 25-Feb-2025. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 30-Apr-2015) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	ressbas.r	$⊢ R = W ↾_{𝑠} A$
		ressbas.b	$⊢ B = {Base}_{W}$
	Assertion	ressbasssOLD	$⊢ {Base}_{R} \subseteq B$

Proof

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		inss2	$⊢ A \cap B \subseteq B$
5	3 4	eqsstrrdi	$⊢ A \in V \to {Base}_{R} \subseteq 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 B$
12	10 11	eqsstrri	$⊢ {Base}_{\emptyset} \subseteq B$
13	9 12	eqsstrdi	$⊢ \neg A \in V \to {Base}_{R} \subseteq B$
14	5 13	pm2.61i	$⊢ {Base}_{R} \subseteq B$