Metamath Proof Explorer


Theorem ressinbas

Description: Restriction only cares about the part of the second set which intersects the base of the first. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypothesis ressid.1 B=BaseW
Assertion ressinbas AXW𝑠A=W𝑠AB

Proof

Step Hyp Ref Expression
1 ressid.1 B=BaseW
2 elex AXAV
3 eqid W𝑠A=W𝑠A
4 3 1 ressid2 BAWVAVW𝑠A=W
5 ssid BB
6 incom AB=BA
7 df-ss BABA=B
8 7 biimpi BABA=B
9 6 8 eqtrid BAAB=B
10 5 9 sseqtrrid BABAB
11 elex WVWV
12 inex1g AVABV
13 eqid W𝑠AB=W𝑠AB
14 13 1 ressid2 BABWVABVW𝑠AB=W
15 10 11 12 14 syl3an BAWVAVW𝑠AB=W
16 4 15 eqtr4d BAWVAVW𝑠A=W𝑠AB
17 16 3expb BAWVAVW𝑠A=W𝑠AB
18 inass ABB=ABB
19 inidm BB=B
20 19 ineq2i ABB=AB
21 18 20 eqtr2i AB=ABB
22 21 opeq2i BasendxAB=BasendxABB
23 22 oveq2i WsSetBasendxAB=WsSetBasendxABB
24 3 1 ressval2 ¬BAWVAVW𝑠A=WsSetBasendxAB
25 inss1 ABA
26 sstr BABABABA
27 25 26 mpan2 BABBA
28 27 con3i ¬BA¬BAB
29 13 1 ressval2 ¬BABWVABVW𝑠AB=WsSetBasendxABB
30 28 11 12 29 syl3an ¬BAWVAVW𝑠AB=WsSetBasendxABB
31 23 24 30 3eqtr4a ¬BAWVAVW𝑠A=W𝑠AB
32 31 3expb ¬BAWVAVW𝑠A=W𝑠AB
33 17 32 pm2.61ian WVAVW𝑠A=W𝑠AB
34 reldmress Reldom𝑠
35 34 ovprc1 ¬WVW𝑠A=
36 34 ovprc1 ¬WVW𝑠AB=
37 35 36 eqtr4d ¬WVW𝑠A=W𝑠AB
38 37 adantr ¬WVAVW𝑠A=W𝑠AB
39 33 38 pm2.61ian AVW𝑠A=W𝑠AB
40 2 39 syl AXW𝑠A=W𝑠AB