stdbdmetval

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

		Ref	Expression
	Hypothesis	stdbdmet.1	$⊢ D = (x \in X, y \in X ⟼ if (x C y \leq R, x C y, R))$
	Assertion	stdbdmetval	$⊢ (R \in V \land A \in X \land B \in X) \to A D B = if (A C B \leq R, A C B, R)$

Step	Hyp	Ref	Expression
1		stdbdmet.1	$⊢ D = (x \in X, y \in X ⟼ if (x C y \leq R, x C y, R))$
2		ovex	$⊢ A C B \in V$
3		ifexg	$⊢ (A C B \in V \land R \in V) \to if (A C B \leq R, A C B, R) \in V$
4	2 3	mpan	$⊢ R \in V \to if (A C B \leq R, A C B, R) \in V$
5		oveq12	$⊢ (x = A \land y = B) \to x C y = A C B$
6	5	breq1d	$⊢ (x = A \land y = B) \to (x C y \leq R \leftrightarrow A C B \leq R)$
7	6 5	ifbieq1d	$⊢ (x = A \land y = B) \to if (x C y \leq R, x C y, R) = if (A C B \leq R, A C B, R)$
8	7 1	ovmpoga	$⊢ (A \in X \land B \in X \land if (A C B \leq R, A C B, R) \in V) \to A D B = if (A C B \leq R, A C B, R)$
9	4 8	syl3an3	$⊢ (A \in X \land B \in X \land R \in V) \to A D B = if (A C B \leq R, A C B, R)$
10	9	3comr	$⊢ (R \in V \land A \in X \land B \in X) \to A D B = if (A C B \leq R, A C B, R)$

Metamath Proof Explorer