xmeterval

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

		Ref	Expression
	Hypothesis	xmeter.1	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
	Assertion	xmeterval	$⊢ D \in ∞Met (X) \to (A \underset{˙}{\sim} B \leftrightarrow (A \in X \land B \in X \land A D B \in ℝ))$

Step	Hyp	Ref	Expression
1		xmeter.1	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
2		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
3		ffn	$⊢ D : X \times X ⟶ ℝ^{*} \to D Fn (X \times X)$
4		elpreima	$⊢ D Fn (X \times X) \to (⟨A, B⟩ \in D^{-1} [ℝ] \leftrightarrow (⟨A, B⟩ \in (X \times X) \land D (⟨A, B⟩) \in ℝ))$
5	2 3 4	3syl	$⊢ D \in ∞Met (X) \to (⟨A, B⟩ \in D^{-1} [ℝ] \leftrightarrow (⟨A, B⟩ \in (X \times X) \land D (⟨A, B⟩) \in ℝ))$
6	1	breqi	$⊢ A \underset{˙}{\sim} B \leftrightarrow A D^{-1} [ℝ] B$
7		df-br	$⊢ A D^{-1} [ℝ] B \leftrightarrow ⟨A, B⟩ \in D^{-1} [ℝ]$
8	6 7	bitri	$⊢ A \underset{˙}{\sim} B \leftrightarrow ⟨A, B⟩ \in D^{-1} [ℝ]$
9		df-3an	$⊢ (A \in X \land B \in X \land A D B \in ℝ) \leftrightarrow ((A \in X \land B \in X) \land A D B \in ℝ)$
10		opelxp	$⊢ ⟨A, B⟩ \in (X \times X) \leftrightarrow (A \in X \land B \in X)$
11	10	bicomi	$⊢ (A \in X \land B \in X) \leftrightarrow ⟨A, B⟩ \in (X \times X)$
12		df-ov	$⊢ A D B = D (⟨A, B⟩)$
13	12	eleq1i	$⊢ A D B \in ℝ \leftrightarrow D (⟨A, B⟩) \in ℝ$
14	11 13	anbi12i	$⊢ ((A \in X \land B \in X) \land A D B \in ℝ) \leftrightarrow (⟨A, B⟩ \in (X \times X) \land D (⟨A, B⟩) \in ℝ)$
15	9 14	bitri	$⊢ (A \in X \land B \in X \land A D B \in ℝ) \leftrightarrow (⟨A, B⟩ \in (X \times X) \land D (⟨A, B⟩) \in ℝ)$
16	5 8 15	3bitr4g	$⊢ D \in ∞Met (X) \to (A \underset{˙}{\sim} B \leftrightarrow (A \in X \land B \in X \land A D B \in ℝ))$

Metamath Proof Explorer