Theorem prdsdsfn

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015)

	Ref	Expression
Hypotheses	prdsbas.p	$$⊢P=S{⨉}_{𝑠}R$$
	prdsbas.s	$$⊢\phi \to S\in V$$
	prdsbas.r	$$⊢\phi \to R\in W$$
	prdsbas.b	$$⊢B={\mathrm{Base}}_P$$
	prdsbas.i	$$⊢\phi \to \mathrm{dom}R=I$$
	prdsds.l	$$⊢D=\mathrm{dist}\left(P\right)$$
Assertion	prdsdsfn	$$⊢\phi \to DFn\left(B\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	$$⊢P=S{⨉}_{𝑠}R$$
2		prdsbas.s	$$⊢\phi \to S\in V$$
3		prdsbas.r	$$⊢\phi \to R\in W$$
4		prdsbas.b	$$⊢B={\mathrm{Base}}_P$$
5		prdsbas.i	$$⊢\phi \to \mathrm{dom}R=I$$
6		prdsds.l	$$⊢D=\mathrm{dist}\left(P\right)$$
7		eqid	$$⊢\left(f\in B,g\in B⟼sup\left(\mathrm{ran}\left(x\in I⟼f\left(x\right)\mathrm{dist}\left(R\left(x\right)\right)g\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)=\left(f\in B,g\in B⟼sup\left(\mathrm{ran}\left(x\in I⟼f\left(x\right)\mathrm{dist}\left(R\left(x\right)\right)g\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$$
8		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
9	8	supex	$$⊢sup\left(\mathrm{ran}\left(x\in I⟼f\left(x\right)\mathrm{dist}\left(R\left(x\right)\right)g\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\in \mathrm{V}$$
10	7 9	fnmpoi	$$⊢\left(f\in B,g\in B⟼sup\left(\mathrm{ran}\left(x\in I⟼f\left(x\right)\mathrm{dist}\left(R\left(x\right)\right)g\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)Fn\left(B\times B\right)$$
11	1 2 3 4 5 6	prdsds	$$⊢\phi \to D=\left(f\in B,g\in B⟼sup\left(\mathrm{ran}\left(x\in I⟼f\left(x\right)\mathrm{dist}\left(R\left(x\right)\right)g\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)$$
12	11	fneq1d	$$⊢\phi \to \left(DFn\left(B\times B\right)\leftrightarrow \left(f\in B,g\in B⟼sup\left(\mathrm{ran}\left(x\in I⟼f\left(x\right)\mathrm{dist}\left(R\left(x\right)\right)g\left(x\right)\right)\cup \left\{0\right\},{ℝ}^{*},<\right)\right)Fn\left(B\times B\right)\right)$$
13	10 12	mpbiri	$$⊢\phi \to DFn\left(B\times B\right)$$