# Metamath Proof Explorer

## Theorem xmeterval

Description: Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis xmeter.1
`|- .~ = ( `' D " RR )`
Assertion xmeterval
`|- ( D e. ( *Met ` X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( A D B ) e. RR ) ) )`

### Proof

Step Hyp Ref Expression
1 xmeter.1
` |-  .~ = ( `' D " RR )`
2 xmetf
` |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )`
3 ffn
` |-  ( D : ( X X. X ) --> RR* -> D Fn ( X X. X ) )`
4 elpreima
` |-  ( D Fn ( X X. X ) -> ( <. A , B >. e. ( `' D " RR ) <-> ( <. A , B >. e. ( X X. X ) /\ ( D ` <. A , B >. ) e. RR ) ) )`
5 2 3 4 3syl
` |-  ( D e. ( *Met ` X ) -> ( <. A , B >. e. ( `' D " RR ) <-> ( <. A , B >. e. ( X X. X ) /\ ( D ` <. A , B >. ) e. RR ) ) )`
6 1 breqi
` |-  ( A .~ B <-> A ( `' D " RR ) B )`
7 df-br
` |-  ( A ( `' D " RR ) B <-> <. A , B >. e. ( `' D " RR ) )`
8 6 7 bitri
` |-  ( A .~ B <-> <. A , B >. e. ( `' D " RR ) )`
9 df-3an
` |-  ( ( A e. X /\ B e. X /\ ( A D B ) e. RR ) <-> ( ( A e. X /\ B e. X ) /\ ( A D B ) e. RR ) )`
10 opelxp
` |-  ( <. A , B >. e. ( X X. X ) <-> ( A e. X /\ B e. X ) )`
11 10 bicomi
` |-  ( ( A e. X /\ B e. X ) <-> <. A , B >. e. ( X X. X ) )`
12 df-ov
` |-  ( A D B ) = ( D ` <. A , B >. )`
13 12 eleq1i
` |-  ( ( A D B ) e. RR <-> ( D ` <. A , B >. ) e. RR )`
14 11 13 anbi12i
` |-  ( ( ( A e. X /\ B e. X ) /\ ( A D B ) e. RR ) <-> ( <. A , B >. e. ( X X. X ) /\ ( D ` <. A , B >. ) e. RR ) )`
15 9 14 bitri
` |-  ( ( A e. X /\ B e. X /\ ( A D B ) e. RR ) <-> ( <. A , B >. e. ( X X. X ) /\ ( D ` <. A , B >. ) e. RR ) )`
16 5 8 15 3bitr4g
` |-  ( D e. ( *Met ` X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( A D B ) e. RR ) ) )`