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