metequiv2

Description: If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Hypotheses	metequiv.3	$⊢ J = MetOpen (C)$
	metequiv.4	$⊢ K = MetOpen (D)$
Assertion	metequiv2	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (\forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land x ball (C) s = x ball (D) s) \to J = K)$

Proof

Step	Hyp	Ref	Expression
1		metequiv.3	$⊢ J = MetOpen (C)$
2		metequiv.4	$⊢ K = MetOpen (D)$
3		simprrr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to x ball (C) s = x ball (D) s$
4		simplll	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to C \in ∞Met (X)$
5		simplr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to x \in X$
6		simprlr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to s \in ℝ^{+}$
7	6	rpxrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to s \in ℝ^{*}$
8		simprll	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to r \in ℝ^{+}$
9	8	rpxrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to r \in ℝ^{*}$
10		simprrl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to s \leq r$
11		ssbl	$⊢ ((C \in ∞Met (X) \land x \in X) \land (s \in ℝ^{} \land r \in ℝ^{}) \land s \leq r) \to x ball (C) s \subseteq x ball (C) r$
12	4 5 7 9 10 11	syl221anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to x ball (C) s \subseteq x ball (C) r$
13	3 12	eqsstrrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to x ball (D) s \subseteq x ball (C) r$
14		simpllr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to D \in ∞Met (X)$
15		ssbl	$⊢ ((D \in ∞Met (X) \land x \in X) \land (s \in ℝ^{} \land r \in ℝ^{}) \land s \leq r) \to x ball (D) s \subseteq x ball (D) r$
16	14 5 7 9 10 15	syl221anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to x ball (D) s \subseteq x ball (D) r$
17	3 16	eqsstrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to x ball (C) s \subseteq x ball (D) r$
18	13 17	jca	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land ((r \in ℝ^{+} \land s \in ℝ^{+}) \land (s \leq r \land x ball (C) s = x ball (D) s))) \to (x ball (D) s \subseteq x ball (C) r \land x ball (C) s \subseteq x ball (D) r)$
19	18	expr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land (r \in ℝ^{+} \land s \in ℝ^{+})) \to ((s \leq r \land x ball (C) s = x ball (D) s) \to (x ball (D) s \subseteq x ball (C) r \land x ball (C) s \subseteq x ball (D) r))$
20	19	anassrs	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land r \in ℝ^{+}) \land s \in ℝ^{+}) \to ((s \leq r \land x ball (C) s = x ball (D) s) \to (x ball (D) s \subseteq x ball (C) r \land x ball (C) s \subseteq x ball (D) r))$
21	20	reximdva	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land r \in ℝ^{+}) \to (\exists s \in ℝ^{+} (s \leq r \land x ball (C) s = x ball (D) s) \to \exists s \in ℝ^{+} (x ball (D) s \subseteq x ball (C) r \land x ball (C) s \subseteq x ball (D) r))$
22		r19.40	$⊢ \exists s \in ℝ^{+} (x ball (D) s \subseteq x ball (C) r \land x ball (C) s \subseteq x ball (D) r) \to (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r)$
23	21 22	syl6	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \land r \in ℝ^{+}) \to (\exists s \in ℝ^{+} (s \leq r \land x ball (C) s = x ball (D) s) \to (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r))$
24	23	ralimdva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land x ball (C) s = x ball (D) s) \to \forall r \in ℝ^{+} (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r))$
25		r19.26	$⊢ \forall r \in ℝ^{+} (\exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r) \leftrightarrow (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r)$
26	24 25	syl6ib	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (X)) \land x \in X) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land x ball (C) s = x ball (D) s) \to (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r))$
27	26	ralimdva	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (\forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land x ball (C) s = x ball (D) s) \to \forall x \in X (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r))$
28	1 2	metequiv	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (J = K \leftrightarrow \forall x \in X (\forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (D) s \subseteq x ball (C) r \land \forall r \in ℝ^{+} \exists s \in ℝ^{+} x ball (C) s \subseteq x ball (D) r))$
29	27 28	sylibrd	$⊢ (C \in ∞Met (X) \land D \in ∞Met (X)) \to (\forall x \in X \forall r \in ℝ^{+} \exists s \in ℝ^{+} (s \leq r \land x ball (C) s = x ball (D) s) \to J = K)$

Metamath Proof Explorer

Theorem metequiv2

Proof