Theorem ressbas

Description: Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014) (Proof shortened by AV, 7-Nov-2024)

	Ref	Expression
Hypotheses	ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
	ressbas.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	ressbas	$$⊢A\in V\to A\cap B={\mathrm{Base}}_R$$

Proof

Step	Hyp	Ref	Expression
1		ressbas.r	$$⊢R=W{\upharpoonright }_{𝑠}A$$
2		ressbas.b	$$⊢B={\mathrm{Base}}_W$$
3		simp1	$$⊢\left(B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to B\subseteq A$$
4		sseqin2	$$⊢B\subseteq A\leftrightarrow A\cap B=B$$
5	3 4	sylib	$$⊢\left(B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to A\cap B=B$$
6	1 2	ressid2	$$⊢\left(B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to R=W$$
7	6	fveq2d	$$⊢\left(B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to {\mathrm{Base}}_R={\mathrm{Base}}_W$$
8	2 5 7	3eqtr4a	$$⊢\left(B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_R$$
9	8	3expib	$$⊢B\subseteq A\to \left(\left(W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_R\right)$$
10		simp2	$$⊢\left(\neg B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to W\in \mathrm{V}$$
11	2	fvexi	$$⊢B\in \mathrm{V}$$
12	11	inex2	$$⊢A\cap B\in \mathrm{V}$$
13		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
14	13	setsid	$$⊢\left(W\in \mathrm{V}\wedge A\cap B\in \mathrm{V}\right)\to A\cap B={\mathrm{Base}}_{\left(W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)}$$
15	10 12 14	sylancl	$$⊢\left(\neg B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_{\left(W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)}$$
16	1 2	ressval2	$$⊢\left(\neg B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to R=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩$$
17	16	fveq2d	$$⊢\left(\neg B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to {\mathrm{Base}}_R={\mathrm{Base}}_{\left(W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap B⟩\right)}$$
18	15 17	eqtr4d	$$⊢\left(\neg B\subseteq A\wedge W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_R$$
19	18	3expib	$$⊢\neg B\subseteq A\to \left(\left(W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_R\right)$$
20	9 19	pm2.61i	$$⊢\left(W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_R$$
21		in0	$$⊢A\cap \varnothing =\varnothing$$
22		fvprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W=\varnothing$$
23	2 22	eqtrid	$$⊢\neg W\in \mathrm{V}\to B=\varnothing$$
24	23	ineq2d	$$⊢\neg W\in \mathrm{V}\to A\cap B=A\cap \varnothing$$
25	21 24 22	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to A\cap B={\mathrm{Base}}_W$$
26		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
27	26	eqcomi	$$⊢{\mathrm{Base}}_{\varnothing }=\varnothing$$
28		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
29	27 1 28	oveqprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W={\mathrm{Base}}_R$$
30	25 29	eqtrd	$$⊢\neg W\in \mathrm{V}\to A\cap B={\mathrm{Base}}_R$$
31	30	adantr	$$⊢\left(\neg W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_R$$
32	20 31	pm2.61ian	$$⊢A\in V\to A\cap B={\mathrm{Base}}_R$$