methaus - Metamath Proof Explorer

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

Theorem methaus 21315

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 21314	. 2
3		metxmet 21129	. . . . . . . . . 10
4	3	ad2antrr 724	. . . . . . . . 9 $/\$ $/\$ $/\$
5		simplrl 762	. . . . . . . . 9 $/\$ $/\$ $/\$
6		metcl 21127	. . . . . . . . . . . . . 14 $/\$ $/\$
7	6	3expb 1198	. . . . . . . . . . . . 13 $/\$ $/\$
8	7	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
9		metgt0 21154	. . . . . . . . . . . . . 14 $/\$ $/\$
10	9	3expb 1198	. . . . . . . . . . . . 13 $/\$ $/\$
11	10	biimpa 482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
12	8, 11	elrpd 11301	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	12	rphalfcld 11316	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	13	rpxrd 11305	. . . . . . . . 9 $/\$ $/\$ $/\$
15		eqid 2402	. . . . . . . . . 10
16	15	blopn 21295	. . . . . . . . 9 $/\$ $/\$
17	4, 5, 14, 16	syl3anc 1230	. . . . . . . 8 $/\$ $/\$ $/\$
18		simplrr 763	. . . . . . . . 9 $/\$ $/\$ $/\$
19	15	blopn 21295	. . . . . . . . 9 $/\$ $/\$
20	4, 18, 14, 19	syl3anc 1230	. . . . . . . 8 $/\$ $/\$ $/\$
21		blcntr 21208	. . . . . . . . 9 $/\$ $/\$
22	4, 5, 13, 21	syl3anc 1230	. . . . . . . 8 $/\$ $/\$ $/\$
23		blcntr 21208	. . . . . . . . 9 $/\$ $/\$
24	4, 18, 13, 23	syl3anc 1230	. . . . . . . 8 $/\$ $/\$ $/\$
25	13	rpred 11304	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26		rexadd 11484	. . . . . . . . . . . 12 $/\$
27	25, 25, 26	syl2anc 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	8	recnd 9652	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
29	28	2halvesd 10825	. . . . . . . . . . 11 $/\$ $/\$ $/\$
30	27, 29	eqtrd 2443	. . . . . . . . . 10 $/\$ $/\$ $/\$
31	8	leidd 10159	. . . . . . . . . 10 $/\$ $/\$ $/\$
32	30, 31	eqbrtrd 4415	. . . . . . . . 9 $/\$ $/\$ $/\$
33		bldisj 21193	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	4, 5, 18, 14, 14, 32, 33	syl33anc 1245	. . . . . . . 8 $/\$ $/\$ $/\$
35		eleq2 2475	. . . . . . . . . 10
36		ineq1 3634	. . . . . . . . . . 11
37	36	eqeq1d 2404	. . . . . . . . . 10
38	35, 37	3anbi13d 1303	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39		eleq2 2475	. . . . . . . . . 10
40		ineq2 3635	. . . . . . . . . . 11
41	40	eqeq1d 2404	. . . . . . . . . 10
42	39, 41	3anbi23d 1304	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
43	38, 42	rspc2ev 3171	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	17, 20, 22, 24, 34, 43	syl113anc 1242	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
45	44	ex 432	. . . . . 6 $/\$ $/\$ $/\$ $/\$
46	45	ralrimivva 2825	. . . . 5 $/\$ $/\$
47	15	mopntopon 21234	. . . . . 6 TopOn
48		ishaus2 20145	. . . . . 6 TopOn $/\$ $/\$
49	3, 47, 48	3syl 18	. . . . 5 $/\$ $/\$
50	46, 49	mpbird 232	. . . 4
51		eleq1 2474	. . . 4
52	50, 51	syl5ibrcom 222	. . 3
53	52	rexlimiv 2890	. 2
54	2, 53	syl 17	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598

wral 2754

wrex 2755

cin 3413

c0 3738 class class class wbr 4395

cfv 5569 (class class class)co 6278

cr 9521

cc0 9522

caddc 9525

cxr 9657

clt 9658

cle 9659

cdiv 10247

c2 10626

crp 11265

cxad 11369

cxmt 18723

cme 18724

cbl 18725

cmopn 18728 TopOnctopon 19687

cha 20102

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599 ax-pre-sup 9600

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2759 df-rex 2760 df-reu 2761 df-rmo 2762 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-pss 3430 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4192 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4490 df-eprel 4734 df-id 4738 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-pred 5367 df-ord 5413 df-on 5414 df-lim 5415 df-suc 5416 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6684 df-1st 6784 df-2nd 6785 df-wrecs 7013 df-recs 7075 df-rdg 7113 df-er 7348 df-map 7459 df-en 7555 df-dom 7556 df-sdom 7557 df-sup 7935 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-div 10248 df-nn 10577 df-2 10635 df-n0 10837 df-z 10906 df-uz 11128 df-q 11228 df-rp 11266 df-xneg 11371 df-xadd 11372 df-xmul 11373 df-icc 11589 df-topgen 15058 df-psmet 18731 df-xmet 18732 df-met 18733 df-bl 18734 df-mopn 18735 df-top 19691 df-bases 19693 df-topon 19694 df-haus 20109

This theorem is referenced by: cnfldhaus 21584 rehaus 21596 metreg 21659 lmcau 22043 cmetss 22045 minveclem4a 22137 minvecolem4a 26207 minvecolem4b 26208 minvecolem4 26210 hlimf 26569 hmopidmchi 27483 rrhcn 28430 rrexthaus 28440 heiborlem9 31597 bfplem1 31600

W3C validator