methaus - Metamath Proof Explorer

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

Theorem methaus 20054

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 20053	. 2
3		metxmet 19868	. . . . . . . . . 10
4	3	ad2antrr 720	. . . . . . . . 9 $/\$ $/\$ $/\$
5		simplrl 754	. . . . . . . . 9 $/\$ $/\$ $/\$
6		metcl 19866	. . . . . . . . . . . . . 14 $/\$ $/\$
7	6	3expb 1183	. . . . . . . . . . . . 13 $/\$ $/\$
8	7	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
9		metgt0 19893	. . . . . . . . . . . . . 14 $/\$ $/\$
10	9	3expb 1183	. . . . . . . . . . . . 13 $/\$ $/\$
11	10	biimpa 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
12	8, 11	elrpd 11021	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	12	rphalfcld 11035	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	13	rpxrd 11024	. . . . . . . . 9 $/\$ $/\$ $/\$
15		eqid 2441	. . . . . . . . . 10
16	15	blopn 20034	. . . . . . . . 9 $/\$ $/\$
17	4, 5, 14, 16	syl3anc 1213	. . . . . . . 8 $/\$ $/\$ $/\$
18		simplrr 755	. . . . . . . . 9 $/\$ $/\$ $/\$
19	15	blopn 20034	. . . . . . . . 9 $/\$ $/\$
20	4, 18, 14, 19	syl3anc 1213	. . . . . . . 8 $/\$ $/\$ $/\$
21		blcntr 19947	. . . . . . . . 9 $/\$ $/\$
22	4, 5, 13, 21	syl3anc 1213	. . . . . . . 8 $/\$ $/\$ $/\$
23		blcntr 19947	. . . . . . . . 9 $/\$ $/\$
24	4, 18, 13, 23	syl3anc 1213	. . . . . . . 8 $/\$ $/\$ $/\$
25	13	rpred 11023	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26		rexadd 11198	. . . . . . . . . . . 12 $/\$
27	25, 25, 26	syl2anc 656	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	8	recnd 9408	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
29	28	2halvesd 10566	. . . . . . . . . . 11 $/\$ $/\$ $/\$
30	27, 29	eqtrd 2473	. . . . . . . . . 10 $/\$ $/\$ $/\$
31	8	leidd 9902	. . . . . . . . . 10 $/\$ $/\$ $/\$
32	30, 31	eqbrtrd 4309	. . . . . . . . 9 $/\$ $/\$ $/\$
33		bldisj 19932	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	4, 5, 18, 14, 14, 32, 33	syl33anc 1228	. . . . . . . 8 $/\$ $/\$ $/\$
35		eleq2 2502	. . . . . . . . . 10
36		ineq1 3542	. . . . . . . . . . 11
37	36	eqeq1d 2449	. . . . . . . . . 10
38	35, 37	3anbi13d 1286	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39		eleq2 2502	. . . . . . . . . 10
40		ineq2 3543	. . . . . . . . . . 11
41	40	eqeq1d 2449	. . . . . . . . . 10
42	39, 41	3anbi23d 1287	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
43	38, 42	rspc2ev 3078	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	17, 20, 22, 24, 34, 43	syl113anc 1225	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
45	44	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$
46	45	ralrimivva 2806	. . . . 5 $/\$ $/\$
47	15	mopntopon 19973	. . . . . 6 TopOn
48		ishaus2 18914	. . . . . 6 TopOn $/\$ $/\$
49	3, 47, 48	3syl 20	. . . . 5 $/\$ $/\$
50	46, 49	mpbird 232	. . . 4
51		eleq1 2501	. . . 4
52	50, 51	syl5ibrcom 222	. . 3
53	52	rexlimiv 2833	. 2
54	2, 53	syl 16	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1364

wcel 1761

wne 2604

wral 2713

wrex 2714

cin 3324

c0 3634 class class class wbr 4289

cfv 5415 (class class class)co 6090

cr 9277

cc0 9278

caddc 9281

cxr 9413

clt 9414

cle 9415

cdiv 9989

c2 10367

crp 10987

cxad 11083

cxmt 17760

cme 17761

cbl 17762

cmopn 17765 TopOnctopon 18458

cha 18871

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-er 7097 df-map 7212 df-en 7307 df-dom 7308 df-sdom 7309 df-sup 7687 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-n0 10576 df-z 10643 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-icc 11303 df-topgen 14378 df-psmet 17768 df-xmet 17769 df-met 17770 df-bl 17771 df-mopn 17772 df-top 18462 df-bases 18464 df-topon 18465 df-haus 18878

This theorem is referenced by: cnfldhaus 20323 rehaus 20335 metreg 20398 lmcau 20782 cmetss 20784 minveclem4a 20876 minvecolem4a 24213 minvecolem4b 24214 minvecolem4 24216 hlimf 24575 hmopidmchi 25490 rrhcn 26362 rrexthaus 26372 heiborlem9 28643 bfplem1 28646

W3C validator