xmetec

Description: The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj , infinity balls are either identical or disjoint, quite unlike the usual situation with Euclidean balls which admit many kinds of overlap. (Contributed by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Hypothesis	xmeter.1	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
	Assertion	xmetec	$⊢ (D \in ∞Met (X) \land P \in X) \to [P] \underset{˙}{\sim} = P ball (D) +∞$

Proof

Step	Hyp	Ref	Expression
1		xmeter.1	$⊢ \underset{˙}{\sim} = D^{-1} [ℝ]$
2	1	xmeterval	$⊢ D \in ∞Met (X) \to (P \underset{˙}{\sim} x \leftrightarrow (P \in X \land x \in X \land P D x \in ℝ))$
3		3anass	$⊢ (P \in X \land x \in X \land P D x \in ℝ) \leftrightarrow (P \in X \land (x \in X \land P D x \in ℝ))$
4	3	baib	$⊢ P \in X \to ((P \in X \land x \in X \land P D x \in ℝ) \leftrightarrow (x \in X \land P D x \in ℝ))$
5	2 4	sylan9bb	$⊢ (D \in ∞Met (X) \land P \in X) \to (P \underset{˙}{\sim} x \leftrightarrow (x \in X \land P D x \in ℝ))$
6		vex	$⊢ x \in V$
7	6	a1i	$⊢ D \in ∞Met (X) \to x \in V$
8		elecg	$⊢ (x \in V \land P \in X) \to (x \in [P] \underset{˙}{\sim} \leftrightarrow P \underset{˙}{\sim} x)$
9	7 8	sylan	$⊢ (D \in ∞Met (X) \land P \in X) \to (x \in [P] \underset{˙}{\sim} \leftrightarrow P \underset{˙}{\sim} x)$
10		xblpnf	$⊢ (D \in ∞Met (X) \land P \in X) \to (x \in (P ball (D) +∞) \leftrightarrow (x \in X \land P D x \in ℝ))$
11	5 9 10	3bitr4d	$⊢ (D \in ∞Met (X) \land P \in X) \to (x \in [P] \underset{˙}{\sim} \leftrightarrow x \in (P ball (D) +∞))$
12	11	eqrdv	$⊢ (D \in ∞Met (X) \land P \in X) \to [P] \underset{˙}{\sim} = P ball (D) +∞$

Metamath Proof Explorer

Theorem xmetec

Proof