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 DFn\left(B\times 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 \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times 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)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 \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times 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)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 \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times 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)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 \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times 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)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\times 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 \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times 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)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(DFn\left(B\times B\right)\leftrightarrow \left(x\in B,y\in B⟼sup\left(\bigcup _{n\in \mathbb{N}}\mathrm{ran}\left(g\in \left\{h\in \left({\left(V\times 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)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\times B\right)\right)$$
13	10 12	mpbiri	$$⊢\phi \to DFn\left(B\times B\right)$$