Description: Any limit of F is also a limit of the restriction of F . (Contributed by Mario Carneiro, 28-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | limcresi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limcrcl | |
|
2 | 1 | simp1d | |
3 | 1 | simp2d | |
4 | 1 | simp3d | |
5 | eqid | |
|
6 | 2 3 4 5 | ellimc2 | |
7 | 6 | ibi | |
8 | inss2 | |
|
9 | difss | |
|
10 | inss2 | |
|
11 | 9 10 | sstri | |
12 | 8 11 | sstri | |
13 | resima2 | |
|
14 | 12 13 | ax-mp | |
15 | inss1 | |
|
16 | ssdif | |
|
17 | 15 16 | ax-mp | |
18 | sslin | |
|
19 | imass2 | |
|
20 | 17 18 19 | mp2b | |
21 | 14 20 | eqsstri | |
22 | sstr | |
|
23 | 21 22 | mpan | |
24 | 23 | anim2i | |
25 | 24 | reximi | |
26 | 25 | imim2i | |
27 | 26 | ralimi | |
28 | 27 | anim2i | |
29 | 7 28 | syl | |
30 | fresin | |
|
31 | 2 30 | syl | |
32 | 15 3 | sstrid | |
33 | 31 32 4 5 | ellimc2 | |
34 | 29 33 | mpbird | |
35 | 34 | ssriv | |