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

Metamath Proof Explorer

Theorem stdbdmetval

Description: Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis stdbdmet.1 ⊢ D = x ∈ X , y ∈ X ⟼ if x C y ≤ R x C y R
Assertion stdbdmetval ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → A D B = if A C B ≤ R A C B R

Proof

Step Hyp Ref Expression
1 stdbdmet.1 ⊢ D = x ∈ X , y ∈ X ⟼ if x C y ≤ R x C y R
2 ovex ⊢ A C B ∈ V
3 ifexg ⊢ A C B ∈ V ∧ R ∈ V → if A C B ≤ R A C B R ∈ V
4 2 3 mpan ⊢ R ∈ V → if A C B ≤ R A C B R ∈ V
5 oveq12 ⊢ x = A ∧ y = B → x C y = A C B
6 5 breq1d ⊢ x = A ∧ y = B → x C y ≤ R ↔ A C B ≤ R
7 6 5 ifbieq1d ⊢ x = A ∧ y = B → if x C y ≤ R x C y R = if A C B ≤ R A C B R
8 7 1 ovmpoga ⊢ A ∈ X ∧ B ∈ X ∧ if A C B ≤ R A C B R ∈ V → A D B = if A C B ≤ R A C B R
9 4 8 syl3an3 ⊢ A ∈ X ∧ B ∈ X ∧ R ∈ V → A D B = if A C B ≤ R A C B R
10 9 3comr ⊢ R ∈ V ∧ A ∈ X ∧ B ∈ X → A D B = if A C B ≤ R A C B R