Theorem ressress

Description: Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014) (Proof shortened by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Assertion	ressress	$$⊢\left(A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simplr	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \neg {\mathrm{Base}}_W\subseteq A$$
2		simpr1	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W\in \mathrm{V}$$
3		simpr2	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\in X$$
4		eqid	$$⊢W{\upharpoonright }_{𝑠}A=W{\upharpoonright }_{𝑠}A$$
5		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
6	4 5	ressval2	$$⊢\left(\neg {\mathrm{Base}}_W\subseteq A\wedge W\in \mathrm{V}\wedge A\in X\right)\to W{\upharpoonright }_{𝑠}A=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩$$
7	1 2 3 6	syl3anc	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}A=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩$$
8		inass	$$⊢\left(A\cap B\right)\cap {\mathrm{Base}}_W=A\cap \left(B\cap {\mathrm{Base}}_W\right)$$
9		in12	$$⊢A\cap \left(B\cap {\mathrm{Base}}_W\right)=B\cap \left(A\cap {\mathrm{Base}}_W\right)$$
10	8 9	eqtri	$$⊢\left(A\cap B\right)\cap {\mathrm{Base}}_W=B\cap \left(A\cap {\mathrm{Base}}_W\right)$$
11	4 5	ressbas	$$⊢A\in X\to A\cap {\mathrm{Base}}_W={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
12	3 11	syl	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\cap {\mathrm{Base}}_W={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
13	12	ineq2d	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to B\cap \left(A\cap {\mathrm{Base}}_W\right)=B\cap {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
14	10 13	eqtr2id	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to B\cap {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}=\left(A\cap B\right)\cap {\mathrm{Base}}_W$$
15	14	opeq2d	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩$$
16	7 15	oveq12d	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}⟩=\left(W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩$$
17		fvex	$$⊢{\mathrm{Base}}_W\in \mathrm{V}$$
18	17	inex2	$$⊢\left(A\cap B\right)\cap {\mathrm{Base}}_W\in \mathrm{V}$$
19		setsabs	$$⊢\left(W\in \mathrm{V}\wedge \left(A\cap B\right)\cap {\mathrm{Base}}_W\in \mathrm{V}\right)\to \left(W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩$$
20	2 18 19	sylancl	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},A\cap {\mathrm{Base}}_W⟩\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩$$
21	16 20	eqtrd	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}⟩=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩$$
22		simpll	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B$$
23		ovexd	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}A\in \mathrm{V}$$
24		simpr3	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to B\in Y$$
25		eqid	$$⊢\left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=\left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B$$
26		eqid	$$⊢{\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
27	25 26	ressval2	$$⊢\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge W{\upharpoonright }_{𝑠}A\in \mathrm{V}\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=\left(W{\upharpoonright }_{𝑠}A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}⟩$$
28	22 23 24 27	syl3anc	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=\left(W{\upharpoonright }_{𝑠}A\right)\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},B\cap {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}⟩$$
29		inss1	$$⊢A\cap B\subseteq A$$
30		sstr	$$⊢\left({\mathrm{Base}}_W\subseteq A\cap B\wedge A\cap B\subseteq A\right)\to {\mathrm{Base}}_W\subseteq A$$
31	29 30	mpan2	$$⊢{\mathrm{Base}}_W\subseteq A\cap B\to {\mathrm{Base}}_W\subseteq A$$
32	1 31	nsyl	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \neg {\mathrm{Base}}_W\subseteq A\cap B$$
33		inex1g	$$⊢A\in X\to A\cap B\in \mathrm{V}$$
34	3 33	syl	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\cap B\in \mathrm{V}$$
35		eqid	$$⊢W{\upharpoonright }_{𝑠}\left(A\cap B\right)=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
36	35 5	ressval2	$$⊢\left(\neg {\mathrm{Base}}_W\subseteq A\cap B\wedge W\in \mathrm{V}\wedge A\cap B\in \mathrm{V}\right)\to W{\upharpoonright }_{𝑠}\left(A\cap B\right)=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩$$
37	32 2 34 36	syl3anc	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}\left(A\cap B\right)=W\mathrm{sSet}⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(A\cap B\right)\cap {\mathrm{Base}}_W⟩$$
38	21 28 37	3eqtr4d	$$⊢\left(\left(\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \neg {\mathrm{Base}}_W\subseteq A\right)\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
39	38	exp31	$$⊢\neg {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\to \left(\neg {\mathrm{Base}}_W\subseteq A\to \left(\left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)\right)\right)$$
40		ovex	$$⊢W{\upharpoonright }_{𝑠}A\in \mathrm{V}$$
41	25 26	ressid2	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge W{\upharpoonright }_{𝑠}A\in \mathrm{V}\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}A$$
42	40 41	mp3an2	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}A$$
43	42	3ad2antr3	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}A$$
44		in32	$$⊢\left(A\cap B\right)\cap {\mathrm{Base}}_W=\left(A\cap {\mathrm{Base}}_W\right)\cap B$$
45		simpr2	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\in X$$
46	45 11	syl	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\cap {\mathrm{Base}}_W={\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}$$
47		simpl	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to {\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B$$
48	46 47	eqsstrd	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\cap {\mathrm{Base}}_W\subseteq B$$
49		df-ss	$$⊢A\cap {\mathrm{Base}}_W\subseteq B\leftrightarrow \left(A\cap {\mathrm{Base}}_W\right)\cap B=A\cap {\mathrm{Base}}_W$$
50	48 49	sylib	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(A\cap {\mathrm{Base}}_W\right)\cap B=A\cap {\mathrm{Base}}_W$$
51	44 50	eqtr2id	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\cap {\mathrm{Base}}_W=\left(A\cap B\right)\cap {\mathrm{Base}}_W$$
52	51	oveq2d	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}\left(A\cap {\mathrm{Base}}_W\right)=W{\upharpoonright }_{𝑠}\left(\left(A\cap B\right)\cap {\mathrm{Base}}_W\right)$$
53	5	ressinbas	$$⊢A\in X\to W{\upharpoonright }_{𝑠}A=W{\upharpoonright }_{𝑠}\left(A\cap {\mathrm{Base}}_W\right)$$
54	45 53	syl	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}A=W{\upharpoonright }_{𝑠}\left(A\cap {\mathrm{Base}}_W\right)$$
55	5	ressinbas	$$⊢A\cap B\in \mathrm{V}\to W{\upharpoonright }_{𝑠}\left(A\cap B\right)=W{\upharpoonright }_{𝑠}\left(\left(A\cap B\right)\cap {\mathrm{Base}}_W\right)$$
56	45 33 55	3syl	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}\left(A\cap B\right)=W{\upharpoonright }_{𝑠}\left(\left(A\cap B\right)\cap {\mathrm{Base}}_W\right)$$
57	52 54 56	3eqtr4d	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}A=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
58	43 57	eqtrd	$$⊢\left({\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
59	58	ex	$$⊢{\mathrm{Base}}_{\left(W{\upharpoonright }_{𝑠}A\right)}\subseteq B\to \left(\left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)\right)$$
60	4 5	ressid2	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge W\in \mathrm{V}\wedge A\in X\right)\to W{\upharpoonright }_{𝑠}A=W$$
61	60	3adant3r3	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}A=W$$
62	61	oveq1d	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}B$$
63		inss2	$$⊢B\cap {\mathrm{Base}}_W\subseteq {\mathrm{Base}}_W$$
64		simpl	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to {\mathrm{Base}}_W\subseteq A$$
65	63 64	sstrid	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to B\cap {\mathrm{Base}}_W\subseteq A$$
66		sseqin2	$$⊢B\cap {\mathrm{Base}}_W\subseteq A\leftrightarrow A\cap \left(B\cap {\mathrm{Base}}_W\right)=B\cap {\mathrm{Base}}_W$$
67	65 66	sylib	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\cap \left(B\cap {\mathrm{Base}}_W\right)=B\cap {\mathrm{Base}}_W$$
68	8 67	eqtr2id	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to B\cap {\mathrm{Base}}_W=\left(A\cap B\right)\cap {\mathrm{Base}}_W$$
69	68	oveq2d	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}\left(B\cap {\mathrm{Base}}_W\right)=W{\upharpoonright }_{𝑠}\left(\left(A\cap B\right)\cap {\mathrm{Base}}_W\right)$$
70		simpr3	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to B\in Y$$
71	5	ressinbas	$$⊢B\in Y\to W{\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(B\cap {\mathrm{Base}}_W\right)$$
72	70 71	syl	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(B\cap {\mathrm{Base}}_W\right)$$
73		simpr2	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to A\in X$$
74	73 33 55	3syl	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}\left(A\cap B\right)=W{\upharpoonright }_{𝑠}\left(\left(A\cap B\right)\cap {\mathrm{Base}}_W\right)$$
75	69 72 74	3eqtr4d	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to W{\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
76	62 75	eqtrd	$$⊢\left({\mathrm{Base}}_W\subseteq A\wedge \left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
77	76	ex	$$⊢{\mathrm{Base}}_W\subseteq A\to \left(\left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)\right)$$
78	39 59 77	pm2.61ii	$$⊢\left(W\in \mathrm{V}\wedge A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
79	78	3expib	$$⊢W\in \mathrm{V}\to \left(\left(A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)\right)$$
80		ress0	$$⊢\varnothing {\upharpoonright }_{𝑠}B=\varnothing$$
81		reldmress	$$⊢\mathrm{Rel}\mathrm{dom}{\upharpoonright }_{𝑠}$$
82	81	ovprc1	$$⊢\neg W\in \mathrm{V}\to W{\upharpoonright }_{𝑠}A=\varnothing$$
83	82	oveq1d	$$⊢\neg W\in \mathrm{V}\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=\varnothing {\upharpoonright }_{𝑠}B$$
84	81	ovprc1	$$⊢\neg W\in \mathrm{V}\to W{\upharpoonright }_{𝑠}\left(A\cap B\right)=\varnothing$$
85	80 83 84	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$
86	85	a1d	$$⊢\neg W\in \mathrm{V}\to \left(\left(A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)\right)$$
87	79 86	pm2.61i	$$⊢\left(A\in X\wedge B\in Y\right)\to \left(W{\upharpoonright }_{𝑠}A\right){\upharpoonright }_{𝑠}B=W{\upharpoonright }_{𝑠}\left(A\cap B\right)$$