methaus - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > methaus		Structured version Unicode version

Theorem methaus 20755

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

**Hypothesis**
Ref	Expression
methaus.1

**Assertion**
Ref	Expression
methaus

Proof of Theorem methaus Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		methaus.1	. . 3
2	1	mopnex 20754	. 2
3		metxmet 20569	. . . . . . . . . 10
4	3	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$
5		simplrl 759	. . . . . . . . 9 $/\$ $/\$ $/\$
6		metcl 20567	. . . . . . . . . . . . . 14 $/\$ $/\$
7	6	3expb 1197	. . . . . . . . . . . . 13 $/\$ $/\$
8	7	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
9		metgt0 20594	. . . . . . . . . . . . . 14 $/\$ $/\$
10	9	3expb 1197	. . . . . . . . . . . . 13 $/\$ $/\$
11	10	biimpa 484	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
12	8, 11	elrpd 11250	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	12	rphalfcld 11264	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	13	rpxrd 11253	. . . . . . . . 9 $/\$ $/\$ $/\$
15		eqid 2467	. . . . . . . . . 10
16	15	blopn 20735	. . . . . . . . 9 $/\$ $/\$
17	4, 5, 14, 16	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$
18		simplrr 760	. . . . . . . . 9 $/\$ $/\$ $/\$
19	15	blopn 20735	. . . . . . . . 9 $/\$ $/\$
20	4, 18, 14, 19	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$
21		blcntr 20648	. . . . . . . . 9 $/\$ $/\$
22	4, 5, 13, 21	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$
23		blcntr 20648	. . . . . . . . 9 $/\$ $/\$
24	4, 18, 13, 23	syl3anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$
25	13	rpred 11252	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26		rexadd 11427	. . . . . . . . . . . 12 $/\$
27	25, 25, 26	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	8	recnd 9618	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
29	28	2halvesd 10780	. . . . . . . . . . 11 $/\$ $/\$ $/\$
30	27, 29	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$ $/\$
31	8	leidd 10115	. . . . . . . . . 10 $/\$ $/\$ $/\$
32	30, 31	eqbrtrd 4467	. . . . . . . . 9 $/\$ $/\$ $/\$
33		bldisj 20633	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	4, 5, 18, 14, 14, 32, 33	syl33anc 1243	. . . . . . . 8 $/\$ $/\$ $/\$
35		eleq2 2540	. . . . . . . . . 10
36		ineq1 3693	. . . . . . . . . . 11
37	36	eqeq1d 2469	. . . . . . . . . 10
38	35, 37	3anbi13d 1301	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39		eleq2 2540	. . . . . . . . . 10
40		ineq2 3694	. . . . . . . . . . 11
41	40	eqeq1d 2469	. . . . . . . . . 10
42	39, 41	3anbi23d 1302	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
43	38, 42	rspc2ev 3225	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	17, 20, 22, 24, 34, 43	syl113anc 1240	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
45	44	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$
46	45	ralrimivva 2885	. . . . 5 $/\$ $/\$
47	15	mopntopon 20674	. . . . . 6 TopOn
48		ishaus2 19615	. . . . . 6 TopOn $/\$ $/\$
49	3, 47, 48	3syl 20	. . . . 5 $/\$ $/\$
50	46, 49	mpbird 232	. . . 4
51		eleq1 2539	. . . 4
52	50, 51	syl5ibrcom 222	. . 3
53	52	rexlimiv 2949	. 2
54	2, 53	syl 16	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767

wne 2662

wral 2814

wrex 2815

cin 3475

c0 3785 class class class wbr 4447

cfv 5586 (class class class)co 6282

cr 9487

cc0 9488

caddc 9491

cxr 9623

clt 9624

cle 9625

cdiv 10202

c2 10581

crp 11216

cxad 11312

cxmt 18171

cme 18172

cbl 18173

cmopn 18176 TopOnctopon 19159

cha 19572

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-er 7308 df-map 7419 df-en 7514 df-dom 7515 df-sdom 7516 df-sup 7897 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-n0 10792 df-z 10861 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-icc 11532 df-topgen 14692 df-psmet 18179 df-xmet 18180 df-met 18181 df-bl 18182 df-mopn 18183 df-top 19163 df-bases 19165 df-topon 19166 df-haus 19579

This theorem is referenced by: cnfldhaus 21024 rehaus 21036 metreg 21099 lmcau 21483 cmetss 21485 minveclem4a 21577 minvecolem4a 25466 minvecolem4b 25467 minvecolem4 25469 hlimf 25828 hmopidmchi 26743 rrhcn 27611 rrexthaus 27621 heiborlem9 29916 bfplem1 29919

W3C validator