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{\upharpoonright }_{𝑠}A$$
	ressbas.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	ressbasssOLD	$$⊢{\mathrm{Base}}_R\subseteq B$$

Proof

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