causs - Metamath Proof Explorer

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

Theorem causs 21605

Description: Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)

**Assertion**
Ref	Expression
causs	$/\$

Proof of Theorem causs Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		caufpm 21589	. . . . . . . . 9 $/\$
2		elfvdm 5898	. . . . . . . . . . 11
3		cnex 9585	. . . . . . . . . . 11
4		elpmg 7446	. . . . . . . . . . 11 $/\$ $/\$
5	2, 3, 4	sylancl 662	. . . . . . . . . 10 $/\$
6	5	biimpa 484	. . . . . . . . 9 $/\$ $/\$
7	1, 6	syldan 470	. . . . . . . 8 $/\$ $/\$
8	7	simprd 463	. . . . . . 7 $/\$
9		rnss 5237	. . . . . . 7
10	8, 9	syl 16	. . . . . 6 $/\$
11		rnxpss 5445	. . . . . 6
12	10, 11	syl6ss 3521	. . . . 5 $/\$
13	12	adantlr 714	. . . 4 $/\$ $/\$
14		frn 5743	. . . . 5
15	14	ad2antlr 726	. . . 4 $/\$ $/\$
16	13, 15	ssind 3727	. . 3 $/\$ $/\$
17	16	ex 434	. 2 $/\$
18		xmetres 20735	. . . . . . . . 9
19		caufpm 21589	. . . . . . . . 9 $/\$
20	18, 19	sylan 471	. . . . . . . 8 $/\$
21		inex1g 4596	. . . . . . . . . . 11
22	2, 21	syl 16	. . . . . . . . . 10
23		elpmg 7446	. . . . . . . . . 10 $/\$ $/\$
24	22, 3, 23	sylancl 662	. . . . . . . . 9 $/\$
25	24	biimpa 484	. . . . . . . 8 $/\$ $/\$
26	20, 25	syldan 470	. . . . . . 7 $/\$ $/\$
27	26	simprd 463	. . . . . 6 $/\$
28		rnss 5237	. . . . . 6
29	27, 28	syl 16	. . . . 5 $/\$
30		rnxpss 5445	. . . . 5
31	29, 30	syl6ss 3521	. . . 4 $/\$
32	31	ex 434	. . 3
33	32	adantr 465	. 2 $/\$
34		ffn 5737	. . . 4
35		df-f 5598	. . . . 5 $/\$
36	35	simplbi2 625	. . . 4
37	34, 36	syl 16	. . 3
38		inss2 3724	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8
40		fss 5745	. . . . . . . 8 $/\$
41	39, 40	sylan2 474	. . . . . . 7 $/\$
42	41	ancoms 453	. . . . . 6 $/\$
43		ffvelrn 6030	. . . . . . . . . . . 12 $/\$
44	43	adantr 465	. . . . . . . . . . 11 $/\$ $/\$
45		eluznn 11164	. . . . . . . . . . . . 13 $/\$
46		ffvelrn 6030	. . . . . . . . . . . . 13 $/\$
47	45, 46	sylan2 474	. . . . . . . . . . . 12 $/\$ $/\$
48	47	anassrs 648	. . . . . . . . . . 11 $/\$ $/\$
49	44, 48	ovresd 6438	. . . . . . . . . 10 $/\$ $/\$
50	49	breq1d 4463	. . . . . . . . 9 $/\$ $/\$
51	50	ralbidva 2903	. . . . . . . 8 $/\$
52	51	rexbidva 2975	. . . . . . 7
53	52	ralbidv 2906	. . . . . 6
54	42, 53	syl 16	. . . . 5 $/\$
55		nnuz 11129	. . . . . 6
56	18	adantr 465	. . . . . 6 $/\$
57		1zzd 10907	. . . . . 6 $/\$
58		eqidd 2468	. . . . . 6 $/\$ $/\$
59		eqidd 2468	. . . . . 6 $/\$ $/\$
60		simpr 461	. . . . . 6 $/\$
61	55, 56, 57, 58, 59, 60	iscauf 21587	. . . . 5 $/\$
62		simpl 457	. . . . . 6 $/\$
63		id 22	. . . . . . 7
64		inss1 3723	. . . . . . . 8
65	64	a1i 11	. . . . . . 7
66		fss 5745	. . . . . . 7 $/\$
67	63, 65, 66	syl2anr 478	. . . . . 6 $/\$
68	55, 62, 57, 58, 59, 67	iscauf 21587	. . . . 5 $/\$
69	54, 61, 68	3bitr4rd 286	. . . 4 $/\$
70	69	ex 434	. . 3
71	37, 70	sylan9r 658	. 2 $/\$
72	17, 33, 71	pm5.21ndd 354	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wcel 1767

wral 2817

wrex 2818

cvv 3118

cin 3480

wss 3481 class class class wbr 4453

cxp 5003

cdm 5005

crn 5006

cres 5007

wfun 5588

wfn 5589

wf 5590

cfv 5594 (class class class)co 6295

cpm 7433

cc 9502

c1 9505

clt 9640

cn 10548

cuz 11094

crp 11232

cxmt 18273

cca 21560

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 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580 ax-pre-mulgt0 9581

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 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6696 df-1st 6795 df-2nd 6796 df-recs 7054 df-rdg 7088 df-er 7323 df-map 7434 df-pm 7435 df-en 7529 df-dom 7530 df-sdom 7531 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-div 10219 df-nn 10549 df-2 10606 df-z 10877 df-uz 11095 df-rp 11233 df-xneg 11330 df-xadd 11331 df-psmet 18281 df-xmet 18282 df-bl 18284 df-cau 21563

This theorem is referenced by: minvecolem4a 25616 hhsscms 26018

W3C validator