Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | climcn1.1 | |
|
climcn1.2 | |
||
climcn1.3 | |
||
climcn1.4 | |
||
climcn1.5 | |
||
climcn1.6 | |
||
climcn1.7 | |
||
climcn1.8 | |
||
climcn1.9 | |
||
Assertion | climcn1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | climcn1.1 | |
|
2 | climcn1.2 | |
|
3 | climcn1.3 | |
|
4 | climcn1.4 | |
|
5 | climcn1.5 | |
|
6 | climcn1.6 | |
|
7 | climcn1.7 | |
|
8 | climcn1.8 | |
|
9 | climcn1.9 | |
|
10 | 2 | adantr | |
11 | simpr | |
|
12 | eqidd | |
|
13 | 5 | adantr | |
14 | 1 10 11 12 13 | climi2 | |
15 | 1 | uztrn2 | |
16 | 8 | adantlr | |
17 | fvoveq1 | |
|
18 | 17 | breq1d | |
19 | 18 | imbrov2fvoveq | |
20 | 19 | rspcva | |
21 | 16 20 | sylan | |
22 | 21 | an32s | |
23 | 15 22 | sylan2 | |
24 | 23 | anassrs | |
25 | 24 | ralimdva | |
26 | 25 | reximdva | |
27 | 26 | ex | |
28 | 14 27 | mpid | |
29 | 28 | rexlimdva | |
30 | 29 | adantr | |
31 | 7 30 | mpd | |
32 | 31 | ralrimiva | |
33 | fveq2 | |
|
34 | 33 | eleq1d | |
35 | 4 | ralrimiva | |
36 | 34 35 3 | rspcdva | |
37 | fveq2 | |
|
38 | 37 | eleq1d | |
39 | 35 | adantr | |
40 | 38 39 8 | rspcdva | |
41 | 1 2 6 9 36 40 | clim2c | |
42 | 32 41 | mpbird | |