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 -1
Assertion xmeterval D ∞Met X A ˙ B A X B X A D B

Proof

Step Hyp Ref Expression
1 xmeter.1 ˙ = D -1
2 xmetf D ∞Met X D : X × X *
3 ffn D : X × X * D Fn X × X
4 elpreima D Fn X × X A B D -1 A B X × X D A B
5 2 3 4 3syl D ∞Met X A B D -1 A B X × X D A B
6 1 breqi A ˙ B A D -1 B
7 df-br A D -1 B A B D -1
8 6 7 bitri A ˙ B A B D -1
9 df-3an A X B X A D B A X B X A D B
10 opelxp A B X × X A X B X
11 10 bicomi A X B X A B X × X
12 df-ov A D B = D A B
13 12 eleq1i A D B D A B
14 11 13 anbi12i A X B X A D B A B X × X D A B
15 9 14 bitri A X B X A D B A B X × X D A B
16 5 8 15 3bitr4g D ∞Met X A ˙ B A X B X A D B