# 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 ${⊢}{\phi }\to {U}={F}{“}_{𝑠}{R}$
imasbas.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{R}}$
imasbas.f ${⊢}{\phi }\to {F}:{V}\underset{onto}{⟶}{B}$
imasbas.r ${⊢}{\phi }\to {R}\in {Z}$
imasds.e ${⊢}{E}=\mathrm{dist}\left({R}\right)$
imasds.d ${⊢}{D}=\mathrm{dist}\left({U}\right)$
Assertion imasdsfn ${⊢}{\phi }\to {D}Fn\left({B}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 imasbas.u ${⊢}{\phi }\to {U}={F}{“}_{𝑠}{R}$
2 imasbas.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{R}}$
3 imasbas.f ${⊢}{\phi }\to {F}:{V}\underset{onto}{⟶}{B}$
4 imasbas.r ${⊢}{\phi }\to {R}\in {Z}$
5 imasds.e ${⊢}{E}=\mathrm{dist}\left({R}\right)$
6 imasds.d ${⊢}{D}=\mathrm{dist}\left({U}\right)$
7 eqid ${⊢}\left({x}\in {B},{y}\in {B}⟼sup\left(\bigcup _{{n}\in ℕ}\mathrm{ran}\left({g}\in \left\{{h}\in \left({\left({V}×{V}\right)}^{\left(1\dots {n}\right)}\right)|\left({F}\left({1}^{st}\left({h}\left(1\right)\right)\right)={x}\wedge {F}\left({2}^{nd}\left({h}\left({n}\right)\right)\right)={y}\wedge \forall {i}\in \left(1\dots {n}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({2}^{nd}\left({h}\left({i}\right)\right)\right)={F}\left({1}^{st}\left({h}\left({i}+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left({E}\circ {g}\right)\right),{ℝ}^{*},<\right)\right)=\left({x}\in {B},{y}\in {B}⟼sup\left(\bigcup _{{n}\in ℕ}\mathrm{ran}\left({g}\in \left\{{h}\in \left({\left({V}×{V}\right)}^{\left(1\dots {n}\right)}\right)|\left({F}\left({1}^{st}\left({h}\left(1\right)\right)\right)={x}\wedge {F}\left({2}^{nd}\left({h}\left({n}\right)\right)\right)={y}\wedge \forall {i}\in \left(1\dots {n}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({2}^{nd}\left({h}\left({i}\right)\right)\right)={F}\left({1}^{st}\left({h}\left({i}+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left({E}\circ {g}\right)\right),{ℝ}^{*},<\right)\right)$
8 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
9 8 infex ${⊢}sup\left(\bigcup _{{n}\in ℕ}\mathrm{ran}\left({g}\in \left\{{h}\in \left({\left({V}×{V}\right)}^{\left(1\dots {n}\right)}\right)|\left({F}\left({1}^{st}\left({h}\left(1\right)\right)\right)={x}\wedge {F}\left({2}^{nd}\left({h}\left({n}\right)\right)\right)={y}\wedge \forall {i}\in \left(1\dots {n}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({2}^{nd}\left({h}\left({i}\right)\right)\right)={F}\left({1}^{st}\left({h}\left({i}+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left({E}\circ {g}\right)\right),{ℝ}^{*},<\right)\in \mathrm{V}$
10 7 9 fnmpoi ${⊢}\left({x}\in {B},{y}\in {B}⟼sup\left(\bigcup _{{n}\in ℕ}\mathrm{ran}\left({g}\in \left\{{h}\in \left({\left({V}×{V}\right)}^{\left(1\dots {n}\right)}\right)|\left({F}\left({1}^{st}\left({h}\left(1\right)\right)\right)={x}\wedge {F}\left({2}^{nd}\left({h}\left({n}\right)\right)\right)={y}\wedge \forall {i}\in \left(1\dots {n}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({2}^{nd}\left({h}\left({i}\right)\right)\right)={F}\left({1}^{st}\left({h}\left({i}+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left({E}\circ {g}\right)\right),{ℝ}^{*},<\right)\right)Fn\left({B}×{B}\right)$
11 1 2 3 4 5 6 imasds ${⊢}{\phi }\to {D}=\left({x}\in {B},{y}\in {B}⟼sup\left(\bigcup _{{n}\in ℕ}\mathrm{ran}\left({g}\in \left\{{h}\in \left({\left({V}×{V}\right)}^{\left(1\dots {n}\right)}\right)|\left({F}\left({1}^{st}\left({h}\left(1\right)\right)\right)={x}\wedge {F}\left({2}^{nd}\left({h}\left({n}\right)\right)\right)={y}\wedge \forall {i}\in \left(1\dots {n}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({2}^{nd}\left({h}\left({i}\right)\right)\right)={F}\left({1}^{st}\left({h}\left({i}+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left({E}\circ {g}\right)\right),{ℝ}^{*},<\right)\right)$
12 11 fneq1d ${⊢}{\phi }\to \left({D}Fn\left({B}×{B}\right)↔\left({x}\in {B},{y}\in {B}⟼sup\left(\bigcup _{{n}\in ℕ}\mathrm{ran}\left({g}\in \left\{{h}\in \left({\left({V}×{V}\right)}^{\left(1\dots {n}\right)}\right)|\left({F}\left({1}^{st}\left({h}\left(1\right)\right)\right)={x}\wedge {F}\left({2}^{nd}\left({h}\left({n}\right)\right)\right)={y}\wedge \forall {i}\in \left(1\dots {n}-1\right)\phantom{\rule{.4em}{0ex}}{F}\left({2}^{nd}\left({h}\left({i}\right)\right)\right)={F}\left({1}^{st}\left({h}\left({i}+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left({E}\circ {g}\right)\right),{ℝ}^{*},<\right)\right)Fn\left({B}×{B}\right)\right)$
13 10 12 mpbiri ${⊢}{\phi }\to {D}Fn\left({B}×{B}\right)$