Theorem methausi 7878

Description: The topology generated by a metric space is Hausdorff. Remark in [Munkres] p. 126.

Hypotheses

Ref	Expression
methausi.1	|- D e. Met
methausi.2	|- J = (Open` D)

Assertion

Ref	Expression
methausi	|- J e. Haus

Proof of Theorem methausi

Step	Hyp	Ref	Expression
1		methausi.1	. . . 4 |- D e. Met
2		eqid 1478	. . . . 5 |- dom dom D = dom dom D
3		methausi.2	. . . . 5 |- J = (Open` D)
4	2, 3	uniopn 7858	. . . 4 |- (D e. Met -> U.J = dom dom D)
5	1, 4	ax-mp 7	. . 3 |- U.J = dom dom D
6	5	eqcomi 1482	. 2 |- dom dom D = U.J
7	3	opntop 7867	. . 3 |- (D e. Met -> J e. Top)
8	1, 7	ax-mp 7	. 2 |- J e. Top
9		eleq2 1538	. . . . 5 |- (n = (x( ball ` D)((xDy) / 2)) -> (x e. n <-> x e. (x( ball ` D)((xDy) / 2))))
10		ineq1 2213	. . . . . 6 |- (n = (x( ball ` D)((xDy) / 2)) -> (n i^i m) = ((x( ball ` D)((xDy) / 2)) i^i m))
11	10	eqeq1d 1486	. . . . 5 |- (n = (x( ball ` D)((xDy) / 2)) -> ((n i^i m) = (/) <-> ((x( ball ` D)((xDy) / 2)) i^i m) = (/)))
12	9, 11	3anbi13d 897	. . . 4 |- (n = (x( ball ` D)((xDy) / 2)) -> ((x e. n /\ y e. m /\ (n i^i m) = (/)) <-> (x e. (x( ball ` D)((xDy) / 2)) /\ y e. m /\ ((x( ball ` D)((xDy) / 2)) i^i m) = (/))))
13		eleq2 1538	. . . . 5 |- (m = (y( ball ` D)((xDy) / 2)) -> (y e. m <-> y e. (y( ball ` D)((xDy) / 2))))
14		ineq2 2214	. . . . . 6 |- (m = (y( ball ` D)((xDy) / 2)) -> ((x( ball ` D)((xDy) / 2)) i^i m) = ((x( ball ` D)((xDy) / 2)) i^i (y( ball ` D)((xDy) / 2))))
15	14	eqeq1d 1486	. . . . 5 |- (m = (y( ball ` D)((xDy) / 2)) -> (((x( ball ` D)((xDy) / 2)) i^i m) = (/) <-> ((x( ball ` D)((xDy) / 2)) i^i (y( ball ` D)((xDy) / 2))) = (/)))
16	13, 15	3anbi23d 898	. . . 4 |- (m = (y( ball ` D)((xDy) / 2)) -> ((x e. (x( ball ` D)((xDy) / 2)) /\ y e. m /\ ((x( ball ` D)((xDy) / 2)) i^i m) = (/)) <-> (x e. (x( ball ` D)((xDy) / 2)) /\ y e. (y( ball ` D)((xDy) / 2)) /\ ((x( ball ` D)((xDy) / 2)) i^i (y( ball ` D)((xDy) / 2))) = (/))))
17	12, 16	rcla42ev 1884	. . 3 |- (((x( ball ` D)((xDy) / 2)) e. J /\ (y( ball ` D)((xDy) / 2)) e. J /\ (x e. (x( ball ` D)((xDy) / 2)) /\ y e. (y( ball ` D)((xDy) / 2)) /\ ((x( ball ` D)((xDy) / 2)) i^i (y( ball ` D)((xDy) / 2))) = (/))) -> E.n e. J E.m e. J (x e. n /\ y e. m /\ (n i^i m) = (/)))
18	2, 3	blopn 7873	. . . . 5 |- (((D e. Met /\ x e. dom dom D) /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> (x( ball ` D)((xDy) / 2)) e. J)
19	1, 18	mpanl1 708	. . . 4 |- ((x e. dom dom D /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> (x( ball ` D)((xDy) / 2)) e. J)
20		3simp1 790	. . . 4 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> x e. dom dom D)
21	2	metcl 7808	. . . . . . . 8 |- ((D e. Met /\ x e. dom dom D /\ y e. dom dom D) -> (xDy) e. RR)
22	1, 21	mp3an1 905	. . . . . . 7 |- ((x e. dom dom D /\ y e. dom dom D) -> (xDy) e. RR)
23		rehalfclt 6036	. . . . . . 7 |- ((xDy) e. RR -> ((xDy) / 2) e. RR)
24	22, 23	syl 10	. . . . . 6 |- ((x e. dom dom D /\ y e. dom dom D) -> ((xDy) / 2) e. RR)
25	24	3adant3 801	. . . . 5 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> ((xDy) / 2) e. RR)
26	2	metgt0 7817	. . . . . . . 8 |- ((D e. Met /\ x e. dom dom D /\ y e. dom dom D) -> (x =/= y <-> 0 < (xDy)))
27	1, 26	mp3an1 905	. . . . . . 7 |- ((x e. dom dom D /\ y e. dom dom D) -> (x =/= y <-> 0 < (xDy)))
28	27	biimp3a 921	. . . . . 6 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> 0 < (xDy))
29		halfpos2t 6039	. . . . . . . 8 |- ((xDy) e. RR -> (0 < (xDy) <-> 0 < ((xDy) / 2)))
30	22, 29	syl 10	. . . . . . 7 |- ((x e. dom dom D /\ y e. dom dom D) -> (0 < (xDy) <-> 0 < ((xDy) / 2)))
31	30	3adant3 801	. . . . . 6 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> (0 < (xDy) <-> 0 < ((xDy) / 2)))
32	28, 31	mpbid 195	. . . . 5 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> 0 < ((xDy) / 2))
33	25, 32	jca 288	. . . 4 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2)))
34	19, 20, 33	sylanc 473	. . 3 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> (x( ball ` D)((xDy) / 2)) e. J)
35	2, 3	blopn 7873	. . . . 5 |- (((D e. Met /\ y e. dom dom D) /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> (y( ball ` D)((xDy) / 2)) e. J)
36	1, 35	mpanl1 708	. . . 4 |- ((y e. dom dom D /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> (y( ball ` D)((xDy) / 2)) e. J)
37		3simp2 791	. . . 4 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> y e. dom dom D)
38	36, 37, 33	sylanc 473	. . 3 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> (y( ball ` D)((xDy) / 2)) e. J)
39	2	blcntr 7842	. . . . . 6 |- (((D e. Met /\ x e. dom dom D) /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> x e. (x( ball ` D)((xDy) / 2)))
40	1, 39	mpanl1 708	. . . . 5 |- ((x e. dom dom D /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> x e. (x( ball ` D)((xDy) / 2)))
41	40, 20, 33	sylanc 473	. . . 4 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> x e. (x( ball ` D)((xDy) / 2)))
42	2	blcntr 7842	. . . . . 6 |- (((D e. Met /\ y e. dom dom D) /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> y e. (y( ball ` D)((xDy) / 2)))
43	1, 42	mpanl1 708	. . . . 5 |- ((y e. dom dom D /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2))) -> y e. (y( ball ` D)((xDy) / 2)))
44	43, 37, 33	sylanc 473	. . . 4 |- ((x e. dom dom D /\ y e. dom dom D /\ x =/= y) -> y e. (y( ball ` D)((xDy) / 2)))
45	2	bl2in 7840	. . . . . 6 |- (((D e. Met /\ x e. dom dom D /\ y e. dom dom D) /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2) /\ ((xDy) / 2) <_ ((xDy) / 2))) -> ((x( ball ` D)((xDy) / 2)) i^i (y( ball ` D)((xDy) / 2))) = (/))
46	1, 45	mp3anl1 912	. . . . 5 |- (((x e. dom dom D /\ y e. dom dom D) /\ (((xDy) / 2) e. RR /\ 0 < ((xDy) / 2) /\ ((xDy) / 2) <_ ((xDy) / 2))) -> ((x( ball ` D)((xDy) / 2)) i^i (y( ball ` D)((x