Theorem ressbas

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

	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		0fv	$$⊢\varnothing \left({\mathrm{Base}}_{\mathrm{ndx}}\right)=\varnothing$$
22		0ex	$$⊢\varnothing \in \mathrm{V}$$
23	22 13	strfvn	$$⊢{\mathrm{Base}}_{\varnothing }=\varnothing \left({\mathrm{Base}}_{\mathrm{ndx}}\right)$$
24		in0	$$⊢A\cap \varnothing =\varnothing$$
25	21 23 24	3eqtr4ri	$$⊢A\cap \varnothing ={\mathrm{Base}}_{\varnothing }$$
26		fvprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W=\varnothing$$
27	2 26	syl5eq	$$⊢\neg W\in \mathrm{V}\to B=\varnothing$$
28	27	ineq2d	$$⊢\neg W\in \mathrm{V}\to A\cap B=A\cap \varnothing$$
29		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
30	29	ovprc1	$$⊢\neg W\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A=\varnothing$$
31	1 30	syl5eq	$$⊢\neg W\in \mathrm{V}\to R=\varnothing$$
32	31	fveq2d	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_R={\mathrm{Base}}_{\varnothing }$$
33	25 28 32	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to A\cap B={\mathrm{Base}}_R$$
34	33	adantr	$$⊢\left(\neg W\in \mathrm{V}\wedge A\in V\right)\to A\cap B={\mathrm{Base}}_R$$
35	20 34	pm2.61ian	$$⊢A\in V\to A\cap B={\mathrm{Base}}_R$$