Theorem xpsdsfn2

Description: Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Hypotheses	xpsds.t	$$⊢T=R{\times }_{𝑠}S$$
	xpsds.x	$$⊢X={\mathrm{Base}}_R$$
	xpsds.y	$$⊢Y={\mathrm{Base}}_S$$
	xpsds.1	$$⊢\phi \to R\in V$$
	xpsds.2	$$⊢\phi \to S\in W$$
	xpsds.p	$$⊢P=\mathrm{dist}\left(T\right)$$
Assertion	xpsdsfn2	$$⊢\phi \to PFn\left({\mathrm{Base}}_T\times {\mathrm{Base}}_T\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpsds.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpsds.x	$$⊢X={\mathrm{Base}}_R$$
3		xpsds.y	$$⊢Y={\mathrm{Base}}_S$$
4		xpsds.1	$$⊢\phi \to R\in V$$
5		xpsds.2	$$⊢\phi \to S\in W$$
6		xpsds.p	$$⊢P=\mathrm{dist}\left(T\right)$$
7	1 2 3 4 5 6	xpsdsfn	$$⊢\phi \to PFn\left(\left(X\times Y\right)\times \left(X\times Y\right)\right)$$
8	1 2 3 4 5	xpsbas	$$⊢\phi \to X\times Y={\mathrm{Base}}_T$$
9	8	sqxpeqd	$$⊢\phi \to \left(X\times Y\right)\times \left(X\times Y\right)={\mathrm{Base}}_T\times {\mathrm{Base}}_T$$
10	9	fneq2d	$$⊢\phi \to \left(PFn\left(\left(X\times Y\right)\times \left(X\times Y\right)\right)\leftrightarrow PFn\left({\mathrm{Base}}_T\times {\mathrm{Base}}_T\right)\right)$$
11	7 10	mpbid	$$⊢\phi \to PFn\left({\mathrm{Base}}_T\times {\mathrm{Base}}_T\right)$$