Metamath Proof Explorer


Theorem metdsre

Description: The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypothesis metdscn.f F=xXsupranySxDy*<
Assertion metdsre DMetXSXSF:X

Proof

Step Hyp Ref Expression
1 metdscn.f F=xXsupranySxDy*<
2 n0 SzzS
3 metxmet DMetXD∞MetX
4 1 metdsf D∞MetXSXF:X0+∞
5 3 4 sylan DMetXSXF:X0+∞
6 5 adantr DMetXSXzSF:X0+∞
7 6 ffnd DMetXSXzSFFnX
8 5 adantr DMetXSXzSwXF:X0+∞
9 simprr DMetXSXzSwXwX
10 8 9 ffvelrnd DMetXSXzSwXFw0+∞
11 eliccxr Fw0+∞Fw*
12 10 11 syl DMetXSXzSwXFw*
13 simpll DMetXSXzSwXDMetX
14 simpr DMetXSXSX
15 14 sselda DMetXSXzSzX
16 15 adantrr DMetXSXzSwXzX
17 metcl DMetXzXwXzDw
18 13 16 9 17 syl3anc DMetXSXzSwXzDw
19 elxrge0 Fw0+∞Fw*0Fw
20 19 simprbi Fw0+∞0Fw
21 10 20 syl DMetXSXzSwX0Fw
22 1 metdsle D∞MetXSXzSwXFwzDw
23 3 22 sylanl1 DMetXSXzSwXFwzDw
24 xrrege0 Fw*zDw0FwFwzDwFw
25 12 18 21 23 24 syl22anc DMetXSXzSwXFw
26 25 anassrs DMetXSXzSwXFw
27 26 ralrimiva DMetXSXzSwXFw
28 ffnfv F:XFFnXwXFw
29 7 27 28 sylanbrc DMetXSXzSF:X
30 29 ex DMetXSXzSF:X
31 30 exlimdv DMetXSXzzSF:X
32 2 31 syl5bi DMetXSXSF:X
33 32 3impia DMetXSXSF:X