methaus - Metamath Proof Explorer

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

Theorem methaus 20222

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 20221	. 2
3		metxmet 20036	. . . . . . . . . 10
4	3	ad2antrr 725	. . . . . . . . 9 $/\$ $/\$ $/\$
5		simplrl 759	. . . . . . . . 9 $/\$ $/\$ $/\$
6		metcl 20034	. . . . . . . . . . . . . 14 $/\$ $/\$
7	6	3expb 1189	. . . . . . . . . . . . 13 $/\$ $/\$
8	7	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
9		metgt0 20061	. . . . . . . . . . . . . 14 $/\$ $/\$
10	9	3expb 1189	. . . . . . . . . . . . 13 $/\$ $/\$
11	10	biimpa 484	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
12	8, 11	elrpd 11131	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	12	rphalfcld 11145	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	13	rpxrd 11134	. . . . . . . . 9 $/\$ $/\$ $/\$
15		eqid 2452	. . . . . . . . . 10
16	15	blopn 20202	. . . . . . . . 9 $/\$ $/\$
17	4, 5, 14, 16	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$
18		simplrr 760	. . . . . . . . 9 $/\$ $/\$ $/\$
19	15	blopn 20202	. . . . . . . . 9 $/\$ $/\$
20	4, 18, 14, 19	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$
21		blcntr 20115	. . . . . . . . 9 $/\$ $/\$
22	4, 5, 13, 21	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$
23		blcntr 20115	. . . . . . . . 9 $/\$ $/\$
24	4, 18, 13, 23	syl3anc 1219	. . . . . . . 8 $/\$ $/\$ $/\$
25	13	rpred 11133	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26		rexadd 11308	. . . . . . . . . . . 12 $/\$
27	25, 25, 26	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	8	recnd 9518	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
29	28	2halvesd 10676	. . . . . . . . . . 11 $/\$ $/\$ $/\$
30	27, 29	eqtrd 2493	. . . . . . . . . 10 $/\$ $/\$ $/\$
31	8	leidd 10012	. . . . . . . . . 10 $/\$ $/\$ $/\$
32	30, 31	eqbrtrd 4415	. . . . . . . . 9 $/\$ $/\$ $/\$
33		bldisj 20100	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	4, 5, 18, 14, 14, 32, 33	syl33anc 1234	. . . . . . . 8 $/\$ $/\$ $/\$
35		eleq2 2525	. . . . . . . . . 10
36		ineq1 3648	. . . . . . . . . . 11
37	36	eqeq1d 2454	. . . . . . . . . 10
38	35, 37	3anbi13d 1292	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39		eleq2 2525	. . . . . . . . . 10
40		ineq2 3649	. . . . . . . . . . 11
41	40	eqeq1d 2454	. . . . . . . . . 10
42	39, 41	3anbi23d 1293	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
43	38, 42	rspc2ev 3182	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	17, 20, 22, 24, 34, 43	syl113anc 1231	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
45	44	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$
46	45	ralrimivva 2908	. . . . 5 $/\$ $/\$
47	15	mopntopon 20141	. . . . . 6 TopOn
48		ishaus2 19082	. . . . . 6 TopOn $/\$ $/\$
49	3, 47, 48	3syl 20	. . . . 5 $/\$ $/\$
50	46, 49	mpbird 232	. . . 4
51		eleq1 2524	. . . 4
52	50, 51	syl5ibrcom 222	. . 3
53	52	rexlimiv 2935	. 2
54	2, 53	syl 16	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1370

wcel 1758

wne 2645

wral 2796

wrex 2797

cin 3430

c0 3740 class class class wbr 4395

cfv 5521 (class class class)co 6195

cr 9387

cc0 9388

caddc 9391

cxr 9523

clt 9524

cle 9525

cdiv 10099

c2 10477

crp 11097

cxad 11193

cxmt 17921

cme 17922

cbl 17923

cmopn 17926 TopOnctopon 18626

cha 19039

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-cnex 9444 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-mulcom 9452 ax-addass 9453 ax-mulass 9454 ax-distr 9455 ax-i2m1 9456 ax-1ne0 9457 ax-1rid 9458 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 ax-pre-ltadd 9464 ax-pre-mulgt0 9465 ax-pre-sup 9466

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-reu 2803 df-rmo 2804 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-pss 3447 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4195 df-iun 4276 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4489 df-eprel 4735 df-id 4739 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-ord 4825 df-on 4826 df-lim 4827 df-suc 4828 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-riota 6156 df-ov 6198 df-oprab 6199 df-mpt2 6200 df-om 6582 df-1st 6682 df-2nd 6683 df-recs 6937 df-rdg 6971 df-er 7206 df-map 7321 df-en 7416 df-dom 7417 df-sdom 7418 df-sup 7797 df-pnf 9526 df-mnf 9527 df-xr 9528 df-ltxr 9529 df-le 9530 df-sub 9703 df-neg 9704 df-div 10100 df-nn 10429 df-2 10486 df-n0 10686 df-z 10753 df-uz 10968 df-q 11060 df-rp 11098 df-xneg 11195 df-xadd 11196 df-xmul 11197 df-icc 11413 df-topgen 14496 df-psmet 17929 df-xmet 17930 df-met 17931 df-bl 17932 df-mopn 17933 df-top 18630 df-bases 18632 df-topon 18633 df-haus 19046

This theorem is referenced by: cnfldhaus 20491 rehaus 20503 metreg 20566 lmcau 20950 cmetss 20952 minveclem4a 21044 minvecolem4a 24425 minvecolem4b 24426 minvecolem4 24428 hlimf 24787 hmopidmchi 25702 rrhcn 26566 rrexthaus 26576 heiborlem9 28861 bfplem1 28864

W3C validator