# Metamath Proof Explorer

## Theorem xmeterval

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

Ref Expression
Hypothesis xmeter.1 = ( 𝐷 “ ℝ )
Assertion xmeterval ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐴 𝐵 ↔ ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ) )

### Proof

Step Hyp Ref Expression
1 xmeter.1 = ( 𝐷 “ ℝ )
2 xmetf ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
3 ffn ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ*𝐷 Fn ( 𝑋 × 𝑋 ) )
4 elpreima ( 𝐷 Fn ( 𝑋 × 𝑋 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐷 “ ℝ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ℝ ) ) )
5 2 3 4 3syl ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐷 “ ℝ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ℝ ) ) )
6 1 breqi ( 𝐴 𝐵𝐴 ( 𝐷 “ ℝ ) 𝐵 )
7 df-br ( 𝐴 ( 𝐷 “ ℝ ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐷 “ ℝ ) )
8 6 7 bitri ( 𝐴 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐷 “ ℝ ) )
9 df-3an ( ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ↔ ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) )
10 opelxp ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ↔ ( 𝐴𝑋𝐵𝑋 ) )
11 10 bicomi ( ( 𝐴𝑋𝐵𝑋 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
12 df-ov ( 𝐴 𝐷 𝐵 ) = ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
13 12 eleq1i ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ↔ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ℝ )
14 11 13 anbi12i ( ( ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ℝ ) )
15 9 14 bitri ( ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ℝ ) )
16 5 8 15 3bitr4g ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐴 𝐵 ↔ ( 𝐴𝑋𝐵𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ) )