Metamath Proof Explorer


Theorem lmfval

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 JTopOnXtJ=fx|fX𝑝𝑚xXuJxuyranfy:yu

Proof

Step Hyp Ref Expression
1 df-lm t=jTopfx|fj𝑝𝑚xjujxuyranfy:yu
2 simpr JTopOnXj=Jj=J
3 2 unieqd JTopOnXj=Jj=J
4 toponuni JTopOnXX=J
5 4 adantr JTopOnXj=JX=J
6 3 5 eqtr4d JTopOnXj=Jj=X
7 6 oveq1d JTopOnXj=Jj𝑝𝑚=X𝑝𝑚
8 7 eleq2d JTopOnXj=Jfj𝑝𝑚fX𝑝𝑚
9 6 eleq2d JTopOnXj=JxjxX
10 2 raleqdv JTopOnXj=Jujxuyranfy:yuuJxuyranfy:yu
11 8 9 10 3anbi123d JTopOnXj=Jfj𝑝𝑚xjujxuyranfy:yufX𝑝𝑚xXuJxuyranfy:yu
12 11 opabbidv JTopOnXj=Jfx|fj𝑝𝑚xjujxuyranfy:yu=fx|fX𝑝𝑚xXuJxuyranfy:yu
13 topontop JTopOnXJTop
14 df-3an fX𝑝𝑚xXuJxuyranfy:yufX𝑝𝑚xXuJxuyranfy:yu
15 14 opabbii fx|fX𝑝𝑚xXuJxuyranfy:yu=fx|fX𝑝𝑚xXuJxuyranfy:yu
16 opabssxp fx|fX𝑝𝑚xXuJxuyranfy:yuX𝑝𝑚×X
17 15 16 eqsstri fx|fX𝑝𝑚xXuJxuyranfy:yuX𝑝𝑚×X
18 ovex X𝑝𝑚V
19 toponmax JTopOnXXJ
20 xpexg X𝑝𝑚VXJX𝑝𝑚×XV
21 18 19 20 sylancr JTopOnXX𝑝𝑚×XV
22 ssexg fx|fX𝑝𝑚xXuJxuyranfy:yuX𝑝𝑚×XX𝑝𝑚×XVfx|fX𝑝𝑚xXuJxuyranfy:yuV
23 17 21 22 sylancr JTopOnXfx|fX𝑝𝑚xXuJxuyranfy:yuV
24 1 12 13 23 fvmptd2 JTopOnXtJ=fx|fX𝑝𝑚xXuJxuyranfy:yu