Description: The relation "sequence f converges to point y " in a metric space. (Contributed by NM, 7-Sep-2006) (Revised by Mario Carneiro, 21-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | lmfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-lm | |
|
2 | simpr | |
|
3 | 2 | unieqd | |
4 | toponuni | |
|
5 | 4 | adantr | |
6 | 3 5 | eqtr4d | |
7 | 6 | oveq1d | |
8 | 7 | eleq2d | |
9 | 6 | eleq2d | |
10 | 2 | raleqdv | |
11 | 8 9 10 | 3anbi123d | |
12 | 11 | opabbidv | |
13 | topontop | |
|
14 | df-3an | |
|
15 | 14 | opabbii | |
16 | opabssxp | |
|
17 | 15 16 | eqsstri | |
18 | ovex | |
|
19 | toponmax | |
|
20 | xpexg | |
|
21 | 18 19 20 | sylancr | |
22 | ssexg | |
|
23 | 17 21 22 | sylancr | |
24 | 1 12 13 23 | fvmptd2 | |