Theorem imasds

Description: The distance function of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 11-Jul-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised 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	imasds	$$⊢\phi \to D=\left(x\in B,y\in B⟼inf\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)$$

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	$$⊢{+}_R={+}_R$$
8		eqid	$$⊢{\cdot }_R={\cdot }_R$$
9		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12		eqid	$$⊢{\cdot }_{𝑖}\left(R\right)={\cdot }_{𝑖}\left(R\right)$$
13		eqid	$$⊢\mathrm{TopOpen}\left(R\right)=\mathrm{TopOpen}\left(R\right)$$
14		eqid	$$⊢{\le }_R={\le }_R$$
15		eqidd	$$⊢\phi \to \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}$$
16		eqidd	$$⊢\phi \to \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}$$
17		eqidd	$$⊢\phi \to \bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)=\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)$$
18		eqidd	$$⊢\phi \to \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}$$
19		eqidd	$$⊢\phi \to \mathrm{TopOpen}\left(R\right)\mathrm{qTop}F=\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F$$
20		eqidd	$$⊢\phi \to \left(x\in B,y\in B⟼inf\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⟼inf\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)$$
21		eqidd	$$⊢\phi \to \left(F\circ {\le }_R\right)\circ F^{-1}=\left(F\circ {\le }_R\right)\circ F^{-1}$$
22	1 2 7 8 9 10 11 12 13 5 14 15 16 17 18 19 20 21 3 4	imasval	$$⊢\phi \to U=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}$$
23		eqid	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}$$
24	23	imasvalstr	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}\right)\mathrm{Struct}⟨1,12⟩$$
25		dsid	$$⊢\mathrm{dist}=\mathrm{Slot}\mathrm{dist}\left(\mathrm{ndx}\right)$$
26		snsstp3	$$⊢\left\{⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}\subseteq \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}$$
27		ssun2	$$⊢\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}$$
28	26 27	sstri	$$⊢\left\{⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ {\le }_R\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in B,y\in B⟼inf\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)⟩\right\}$$
29		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
30	2 29	eqeltrdi	$$⊢\phi \to V\in \mathrm{V}$$
31		focdmex	$$⊢V\in \mathrm{V}\to \left(F:V\underset{onto}{⟶}B\to B\in \mathrm{V}\right)$$
32	30 3 31	sylc	$$⊢\phi \to B\in \mathrm{V}$$
33		mpoexga	$$⊢\left(B\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(x\in B,y\in B⟼inf\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)\in \mathrm{V}$$
34	32 32 33	syl2anc	$$⊢\phi \to \left(x\in B,y\in B⟼inf\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)\in \mathrm{V}$$
35	22 24 25 28 34 6	strfv3	$$⊢\phi \to D=\left(x\in B,y\in B⟼inf\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)$$