Metamath Proof Explorer


Theorem imasdsfn

Description: The distance function is a function on the base set. (Contributed by Mario Carneiro, 20-Aug-2015) (Proof shortened by AV, 6-Oct-2020)

Ref Expression
Hypotheses imasbas.u φ U = F 𝑠 R
imasbas.v φ V = Base R
imasbas.f φ F : V onto B
imasbas.r φ R Z
imasds.e E = dist R
imasds.d D = dist U
Assertion imasdsfn φ D Fn B × B

Proof

Step Hyp Ref Expression
1 imasbas.u φ U = F 𝑠 R
2 imasbas.v φ V = Base R
3 imasbas.f φ F : V onto B
4 imasbas.r φ R Z
5 imasds.e E = dist R
6 imasds.d D = dist U
7 eqid x B , y B sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * < = x B , y B sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * <
8 xrltso < Or *
9 8 infex sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * < V
10 7 9 fnmpoi x B , y B sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * < Fn B × B
11 1 2 3 4 5 6 imasds φ D = x B , y B sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * <
12 11 fneq1d φ D Fn B × B x B , y B sup n ran g h V × V 1 n | F 1 st h 1 = x F 2 nd h n = y i 1 n 1 F 2 nd h i = F 1 st h i + 1 𝑠 * E g * < Fn B × B
13 10 12 mpbiri φ D Fn B × B