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 | |
|
Assertion | ressinbas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ressid.1 | |
|
2 | elex | |
|
3 | eqid | |
|
4 | 3 1 | ressid2 | |
5 | ssid | |
|
6 | incom | |
|
7 | df-ss | |
|
8 | 7 | biimpi | |
9 | 6 8 | eqtrid | |
10 | 5 9 | sseqtrrid | |
11 | elex | |
|
12 | inex1g | |
|
13 | eqid | |
|
14 | 13 1 | ressid2 | |
15 | 10 11 12 14 | syl3an | |
16 | 4 15 | eqtr4d | |
17 | 16 | 3expb | |
18 | inass | |
|
19 | inidm | |
|
20 | 19 | ineq2i | |
21 | 18 20 | eqtr2i | |
22 | 21 | opeq2i | |
23 | 22 | oveq2i | |
24 | 3 1 | ressval2 | |
25 | inss1 | |
|
26 | sstr | |
|
27 | 25 26 | mpan2 | |
28 | 27 | con3i | |
29 | 13 1 | ressval2 | |
30 | 28 11 12 29 | syl3an | |
31 | 23 24 30 | 3eqtr4a | |
32 | 31 | 3expb | |
33 | 17 32 | pm2.61ian | |
34 | reldmress | |
|
35 | 34 | ovprc1 | |
36 | 34 | ovprc1 | |
37 | 35 36 | eqtr4d | |
38 | 37 | adantr | |
39 | 33 38 | pm2.61ian | |
40 | 2 39 | syl | |