Theorem stdbdmetval

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

	Ref	Expression
Hypothesis	stdbdmet.1	|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
Assertion	stdbdmetval	|- ( ( R e. V /\ A e. X /\ B e. X ) -> ( A D B ) = if ( ( A C B ) <_ R , ( A C B ) , R ) )

Proof

Step	Hyp	Ref	Expression
1		stdbdmet.1	|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )
2		ovex	|- ( A C B ) e. _V
3		ifexg	|- ( ( ( A C B ) e. _V /\ R e. V ) -> if ( ( A C B ) <_ R , ( A C B ) , R ) e. _V )
4	2 3	mpan	|- ( R e. V -> if ( ( A C B ) <_ R , ( A C B ) , R ) e. _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 e. X /\ B e. X /\ if ( ( A C B ) <_ R , ( A C B ) , R ) e. _V ) -> ( A D B ) = if ( ( A C B ) <_ R , ( A C B ) , R ) )
9	4 8	syl3an3	|- ( ( A e. X /\ B e. X /\ R e. V ) -> ( A D B ) = if ( ( A C B ) <_ R , ( A C B ) , R ) )
10	9	3comr	|- ( ( R e. V /\ A e. X /\ B e. X ) -> ( A D B ) = if ( ( A C B ) <_ R , ( A C B ) , R ) )