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