This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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