methaus

Description: The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Hypothesis	methaus.1	$⊢ J = MetOpen (D)$
	Assertion	methaus	$⊢ D \in ∞Met (X) \to J \in Haus$

Proof

Step	Hyp	Ref	Expression
1		methaus.1	$⊢ J = MetOpen (D)$
2	1	mopnex	$⊢ D \in ∞Met (X) \to \exists d \in Met (X) J = MetOpen (d)$
3		metxmet	$⊢ d \in Met (X) \to d \in ∞Met (X)$
4	3	ad2antrr	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to d \in ∞Met (X)$
5		simplrl	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to x \in X$
6		metcl	$⊢ (d \in Met (X) \land x \in X \land y \in X) \to x d y \in ℝ$
7	6	3expb	$⊢ (d \in Met (X) \land (x \in X \land y \in X)) \to x d y \in ℝ$
8	7	adantr	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to x d y \in ℝ$
9		metgt0	$⊢ (d \in Met (X) \land x \in X \land y \in X) \to (x \neq y \leftrightarrow 0 < x d y)$
10	9	3expb	$⊢ (d \in Met (X) \land (x \in X \land y \in X)) \to (x \neq y \leftrightarrow 0 < x d y)$
11	10	biimpa	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to 0 < x d y$
12	8 11	elrpd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to x d y \in ℝ^{+}$
13	12	rphalfcld	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to \frac{x d y}{2} \in ℝ^{+}$
14	13	rpxrd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to \frac{x d y}{2} \in ℝ^{*}$
15		eqid	$⊢ MetOpen (d) = MetOpen (d)$
16	15	blopn	$⊢ (d \in ∞Met (X) \land x \in X \land \frac{x d y}{2} \in ℝ^{*}) \to x ball (d) (\frac{x d y}{2}) \in MetOpen (d)$
17	4 5 14 16	syl3anc	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to x ball (d) (\frac{x d y}{2}) \in MetOpen (d)$
18		simplrr	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to y \in X$
19	15	blopn	$⊢ (d \in ∞Met (X) \land y \in X \land \frac{x d y}{2} \in ℝ^{*}) \to y ball (d) (\frac{x d y}{2}) \in MetOpen (d)$
20	4 18 14 19	syl3anc	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to y ball (d) (\frac{x d y}{2}) \in MetOpen (d)$
21		blcntr	$⊢ (d \in ∞Met (X) \land x \in X \land \frac{x d y}{2} \in ℝ^{+}) \to x \in (x ball (d) (\frac{x d y}{2}))$
22	4 5 13 21	syl3anc	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to x \in (x ball (d) (\frac{x d y}{2}))$
23		blcntr	$⊢ (d \in ∞Met (X) \land y \in X \land \frac{x d y}{2} \in ℝ^{+}) \to y \in (y ball (d) (\frac{x d y}{2}))$
24	4 18 13 23	syl3anc	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to y \in (y ball (d) (\frac{x d y}{2}))$
25	13	rpred	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to \frac{x d y}{2} \in ℝ$
26	25 25	rexaddd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to (\frac{x d y}{2}) +_{𝑒} (\frac{x d y}{2}) = (\frac{x d y}{2}) + (\frac{x d y}{2})$
27	8	recnd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to x d y \in ℂ$
28	27	2halvesd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to (\frac{x d y}{2}) + (\frac{x d y}{2}) = x d y$
29	26 28	eqtrd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to (\frac{x d y}{2}) +_{𝑒} (\frac{x d y}{2}) = x d y$
30	8	leidd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to x d y \leq x d y$
31	29 30	eqbrtrd	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to (\frac{x d y}{2}) +_{𝑒} (\frac{x d y}{2}) \leq x d y$
32		bldisj	$⊢ ((d \in ∞Met (X) \land x \in X \land y \in X) \land (\frac{x d y}{2} \in ℝ^{} \land \frac{x d y}{2} \in ℝ^{} \land (\frac{x d y}{2}) +_{𝑒} (\frac{x d y}{2}) \leq x d y)) \to (x ball (d) (\frac{x d y}{2})) \cap (y ball (d) (\frac{x d y}{2})) = \emptyset$
33	4 5 18 14 14 31 32	syl33anc	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to (x ball (d) (\frac{x d y}{2})) \cap (y ball (d) (\frac{x d y}{2})) = \emptyset$
34		eleq2	$⊢ m = x ball (d) (\frac{x d y}{2}) \to (x \in m \leftrightarrow x \in (x ball (d) (\frac{x d y}{2})))$
35		ineq1	$⊢ m = x ball (d) (\frac{x d y}{2}) \to m \cap n = (x ball (d) (\frac{x d y}{2})) \cap n$
36	35	eqeq1d	$⊢ m = x ball (d) (\frac{x d y}{2}) \to (m \cap n = \emptyset \leftrightarrow (x ball (d) (\frac{x d y}{2})) \cap n = \emptyset)$
37	34 36	3anbi13d	$⊢ m = x ball (d) (\frac{x d y}{2}) \to ((x \in m \land y \in n \land m \cap n = \emptyset) \leftrightarrow (x \in (x ball (d) (\frac{x d y}{2})) \land y \in n \land (x ball (d) (\frac{x d y}{2})) \cap n = \emptyset))$
38		eleq2	$⊢ n = y ball (d) (\frac{x d y}{2}) \to (y \in n \leftrightarrow y \in (y ball (d) (\frac{x d y}{2})))$
39		ineq2	$⊢ n = y ball (d) (\frac{x d y}{2}) \to (x ball (d) (\frac{x d y}{2})) \cap n = (x ball (d) (\frac{x d y}{2})) \cap (y ball (d) (\frac{x d y}{2}))$
40	39	eqeq1d	$⊢ n = y ball (d) (\frac{x d y}{2}) \to ((x ball (d) (\frac{x d y}{2})) \cap n = \emptyset \leftrightarrow (x ball (d) (\frac{x d y}{2})) \cap (y ball (d) (\frac{x d y}{2})) = \emptyset)$
41	38 40	3anbi23d	$⊢ n = y ball (d) (\frac{x d y}{2}) \to ((x \in (x ball (d) (\frac{x d y}{2})) \land y \in n \land (x ball (d) (\frac{x d y}{2})) \cap n = \emptyset) \leftrightarrow (x \in (x ball (d) (\frac{x d y}{2})) \land y \in (y ball (d) (\frac{x d y}{2})) \land (x ball (d) (\frac{x d y}{2})) \cap (y ball (d) (\frac{x d y}{2})) = \emptyset))$
42	37 41	rspc2ev	$⊢ (x ball (d) (\frac{x d y}{2}) \in MetOpen (d) \land y ball (d) (\frac{x d y}{2}) \in MetOpen (d) \land (x \in (x ball (d) (\frac{x d y}{2})) \land y \in (y ball (d) (\frac{x d y}{2})) \land (x ball (d) (\frac{x d y}{2})) \cap (y ball (d) (\frac{x d y}{2})) = \emptyset)) \to \exists m \in MetOpen (d) \exists n \in MetOpen (d) (x \in m \land y \in n \land m \cap n = \emptyset)$
43	17 20 22 24 33 42	syl113anc	$⊢ ((d \in Met (X) \land (x \in X \land y \in X)) \land x \neq y) \to \exists m \in MetOpen (d) \exists n \in MetOpen (d) (x \in m \land y \in n \land m \cap n = \emptyset)$
44	43	ex	$⊢ (d \in Met (X) \land (x \in X \land y \in X)) \to (x \neq y \to \exists m \in MetOpen (d) \exists n \in MetOpen (d) (x \in m \land y \in n \land m \cap n = \emptyset))$
45	44	ralrimivva	$⊢ d \in Met (X) \to \forall x \in X \forall y \in X (x \neq y \to \exists m \in MetOpen (d) \exists n \in MetOpen (d) (x \in m \land y \in n \land m \cap n = \emptyset))$
46	15	mopntopon	$⊢ d \in ∞Met (X) \to MetOpen (d) \in TopOn (X)$
47		ishaus2	$⊢ MetOpen (d) \in TopOn (X) \to (MetOpen (d) \in Haus \leftrightarrow \forall x \in X \forall y \in X (x \neq y \to \exists m \in MetOpen (d) \exists n \in MetOpen (d) (x \in m \land y \in n \land m \cap n = \emptyset)))$
48	3 46 47	3syl	$⊢ d \in Met (X) \to (MetOpen (d) \in Haus \leftrightarrow \forall x \in X \forall y \in X (x \neq y \to \exists m \in MetOpen (d) \exists n \in MetOpen (d) (x \in m \land y \in n \land m \cap n = \emptyset)))$
49	45 48	mpbird	$⊢ d \in Met (X) \to MetOpen (d) \in Haus$
50		eleq1	$⊢ J = MetOpen (d) \to (J \in Haus \leftrightarrow MetOpen (d) \in Haus)$
51	49 50	syl5ibrcom	$⊢ d \in Met (X) \to (J = MetOpen (d) \to J \in Haus)$
52	51	rexlimiv	$⊢ \exists d \in Met (X) J = MetOpen (d) \to J \in Haus$
53	2 52	syl	$⊢ D \in ∞Met (X) \to J \in Haus$

Metamath Proof Explorer

Theorem methaus

Proof