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 ) ) |