caussi - Metamath Proof Explorer

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

Theorem caussi 22345

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

**Assertion**
Ref	Expression
caussi

Proof of Theorem caussi Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3643	. . . . . . . . 9
2		xpss2 4949	. . . . . . . . 9
3	1, 2	ax-mp 5	. . . . . . . 8
4		sstr 3426	. . . . . . . 8 $/\$
5	3, 4	mpan2 685	. . . . . . 7
6	5	anim2i 579	. . . . . 6 $/\$ $/\$
7	6	a1i 11	. . . . 5 $/\$ $/\$
8		elfvdm 5905	. . . . . . 7
9		inex1g 4539	. . . . . . 7
10	8, 9	syl 17	. . . . . 6
11		cnex 9638	. . . . . 6
12		elpmg 7505	. . . . . 6 $/\$ $/\$
13	10, 11, 12	sylancl 675	. . . . 5 $/\$
14		elpmg 7505	. . . . . 6 $/\$ $/\$
15	8, 11, 14	sylancl 675	. . . . 5 $/\$
16	7, 13, 15	3imtr4d 276	. . . 4
17		uzid 11197	. . . . . . . . . 10
18	17	adantl 473	. . . . . . . . 9 $/\$
19		simp2 1031	. . . . . . . . . 10 $/\$ $/\$
20	19	ralimi 2796	. . . . . . . . 9 $/\$ $/\$
21		fveq2 5879	. . . . . . . . . . 11
22	21	eleq1d 2533	. . . . . . . . . 10
23	22	rspcva 3134	. . . . . . . . 9 $/\$
24	18, 20, 23	syl2an 485	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25		inss2 3644	. . . . . . . . . . . . . 14
26		simpr 468	. . . . . . . . . . . . . 14 $/\$ $/\$
27	25, 26	sseldi 3416	. . . . . . . . . . . . 13 $/\$ $/\$
28	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
29	28	sselda 3418	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
30		simplr 770	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
31	29, 30	ovresd 6456	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
32	31	breq1d 4405	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	32	biimpd 212	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34	33	imdistanda 707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
35	1	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
36	35	sseld 3417	. . . . . . . . . . . . . . 15 $/\$ $/\$
37	36	anim1d 574	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
38	34, 37	syld 44	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
39	27, 38	syldan 478	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40	39	anim2d 575	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		3anass 1011	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42		3anass 1011	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	40, 41, 42	3imtr4g 278	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	43	ralimdv 2806	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	44	impancom 447	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	24, 45	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	ex 441	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
48	47	reximdva 2858	. . . . 5 $/\$ $/\$ $/\$ $/\$
49	48	ralimdv 2806	. . . 4 $/\$ $/\$ $/\$ $/\$
50	16, 49	anim12d 572	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		xmetres 21457	. . . 4
52		iscau2 22325	. . . 4 $/\$ $/\$ $/\$
53	51, 52	syl 17	. . 3 $/\$ $/\$ $/\$
54		iscau2 22325	. . 3 $/\$ $/\$ $/\$
55	50, 53, 54	3imtr4d 276	. 2
56	55	ssrdv 3424	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wcel 1904

wral 2756

wrex 2757

cvv 3031

cin 3389

wss 3390 class class class wbr 4395

cxp 4837

cdm 4839

cres 4841

wfun 5583

cfv 5589 (class class class)co 6308

cpm 7491

cc 9555

clt 9693

cz 10961

cuz 11182

crp 11325

cxmt 19032

cca 22301

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-po 4760 df-so 4761 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-1st 6812 df-2nd 6813 df-er 7381 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-neg 9883 df-z 10962 df-uz 11183 df-rp 11326 df-xadd 11433 df-psmet 19039 df-xmet 19040 df-bl 19042 df-cau 22304

This theorem is referenced by: (None)

W3C validator