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 ⊢ ∼ = ( ◡ 𝐷 “ ℝ )
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 ‘ 𝑋 ) → ( 𝐴 ∼ 𝐵 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ) )