caussi - Metamath Proof Explorer

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

Theorem caussi 20939

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 3677	. . . . . . . . 9
2		xpss2 5056	. . . . . . . . 9
3	1, 2	ax-mp 5	. . . . . . . 8
4		sstr 3471	. . . . . . . 8 $/\$
5	3, 4	mpan2 671	. . . . . . 7
6	5	anim2i 569	. . . . . 6 $/\$ $/\$
7	6	a1i 11	. . . . 5 $/\$ $/\$
8		elfvdm 5824	. . . . . . 7
9		inex1g 4542	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11		cnex 9473	. . . . . 6
12		elpmg 7337	. . . . . 6 $/\$ $/\$
13	10, 11, 12	sylancl 662	. . . . 5 $/\$
14		elpmg 7337	. . . . . 6 $/\$ $/\$
15	8, 11, 14	sylancl 662	. . . . 5 $/\$
16	7, 13, 15	3imtr4d 268	. . . 4
17		uzid 10985	. . . . . . . . . 10
18	17	adantl 466	. . . . . . . . 9 $/\$
19		simp2 989	. . . . . . . . . 10 $/\$ $/\$
20	19	ralimi 2818	. . . . . . . . 9 $/\$ $/\$
21		fveq2 5798	. . . . . . . . . . 11
22	21	eleq1d 2523	. . . . . . . . . 10
23	22	rspcva 3175	. . . . . . . . 9 $/\$
24	18, 20, 23	syl2an 477	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25		inss2 3678	. . . . . . . . . . . . . 14
26		simpr 461	. . . . . . . . . . . . . 14 $/\$ $/\$
27	25, 26	sseldi 3461	. . . . . . . . . . . . 13 $/\$ $/\$
28	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
29	28	sselda 3463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
30		simplr 754	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
31	29, 30	ovresd 6340	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
32	31	breq1d 4409	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	32	biimpd 207	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34	33	imdistanda 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
35	1	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
36	35	sseld 3462	. . . . . . . . . . . . . . 15 $/\$ $/\$
37	36	anim1d 564	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
38	34, 37	syld 44	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
39	27, 38	syldan 470	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40	39	anim2d 565	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		3anass 969	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42		3anass 969	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	40, 41, 42	3imtr4g 270	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	43	ralimdv 2833	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	44	impancom 440	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	24, 45	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
48	47	reximdva 2932	. . . . 5 $/\$ $/\$ $/\$ $/\$
49	48	ralimdv 2833	. . . 4 $/\$ $/\$ $/\$ $/\$
50	16, 49	anim12d 563	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		xmetres 20070	. . . 4
52		iscau2 20919	. . . 4 $/\$ $/\$ $/\$
53	51, 52	syl 16	. . 3 $/\$ $/\$ $/\$
54		iscau2 20919	. . 3 $/\$ $/\$ $/\$
55	50, 53, 54	3imtr4d 268	. 2
56	55	ssrdv 3469	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wcel 1758

wral 2798

wrex 2799

cvv 3076

cin 3434

wss 3435 class class class wbr 4399

cxp 4945

cdm 4947

cres 4949

wfun 5519

cfv 5525 (class class class)co 6199

cpm 7324

cc 9390

clt 9528

cz 10756

cuz 10971

crp 11101

cxmt 17925

cca 20895

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 1955 ax-ext 2432 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468

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 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-op 3991 df-uni 4199 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-id 4743 df-po 4748 df-so 4749 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-1st 6686 df-2nd 6687 df-er 7210 df-map 7325 df-pm 7326 df-en 7420 df-dom 7421 df-sdom 7422 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-neg 9708 df-z 10757 df-uz 10972 df-rp 11102 df-xadd 11200 df-psmet 17933 df-xmet 17934 df-bl 17936 df-cau 20898

This theorem is referenced by: (None)

W3C validator