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

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