Metamath Proof Explorer


Theorem prdsdsfn

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

Ref Expression
Hypotheses prdsbas.p P = S 𝑠 R
prdsbas.s φ S V
prdsbas.r φ R W
prdsbas.b B = Base P
prdsbas.i φ dom R = I
prdsds.l D = dist P
Assertion prdsdsfn φ D Fn B × B

Proof

Step Hyp Ref Expression
1 prdsbas.p P = S 𝑠 R
2 prdsbas.s φ S V
3 prdsbas.r φ R W
4 prdsbas.b B = Base P
5 prdsbas.i φ dom R = I
6 prdsds.l D = dist P
7 eqid f B , g B sup ran x I f x dist R x g x 0 * < = f B , g B sup ran x I f x dist R x g x 0 * <
8 xrltso < Or *
9 8 supex sup ran x I f x dist R x g x 0 * < V
10 7 9 fnmpoi f B , g B sup ran x I f x dist R x g x 0 * < Fn B × B
11 1 2 3 4 5 6 prdsds φ D = f B , g B sup ran x I f x dist R x g x 0 * <
12 11 fneq1d φ D Fn B × B f B , g B sup ran x I f x dist R x g x 0 * < Fn B × B
13 10 12 mpbiri φ D Fn B × B