caussi - Metamath Proof Explorer

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

Theorem caussi 21862

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 3714	. . . . . . . . 9
2		xpss2 5121	. . . . . . . . 9
3	1, 2	ax-mp 5	. . . . . . . 8
4		sstr 3507	. . . . . . . 8 $/\$
5	3, 4	mpan2 671	. . . . . . 7
6	5	anim2i 569	. . . . . 6 $/\$ $/\$
7	6	a1i 11	. . . . 5 $/\$ $/\$
8		elfvdm 5898	. . . . . . 7
9		inex1g 4599	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11		cnex 9590	. . . . . 6
12		elpmg 7453	. . . . . 6 $/\$ $/\$
13	10, 11, 12	sylancl 662	. . . . 5 $/\$
14		elpmg 7453	. . . . . 6 $/\$ $/\$
15	8, 11, 14	sylancl 662	. . . . 5 $/\$
16	7, 13, 15	3imtr4d 268	. . . 4
17		uzid 11120	. . . . . . . . . 10
18	17	adantl 466	. . . . . . . . 9 $/\$
19		simp2 997	. . . . . . . . . 10 $/\$ $/\$
20	19	ralimi 2850	. . . . . . . . 9 $/\$ $/\$
21		fveq2 5872	. . . . . . . . . . 11
22	21	eleq1d 2526	. . . . . . . . . 10
23	22	rspcva 3208	. . . . . . . . 9 $/\$
24	18, 20, 23	syl2an 477	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25		inss2 3715	. . . . . . . . . . . . . 14
26		simpr 461	. . . . . . . . . . . . . 14 $/\$ $/\$
27	25, 26	sseldi 3497	. . . . . . . . . . . . 13 $/\$ $/\$
28	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
29	28	sselda 3499	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
30		simplr 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
31	29, 30	ovresd 6442	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
32	31	breq1d 4466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	32	biimpd 207	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34	33	imdistanda 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
35	1	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
36	35	sseld 3498	. . . . . . . . . . . . . . 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 977	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42		3anass 977	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	40, 41, 42	3imtr4g 270	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	43	ralimdv 2867	. . . . . . . . 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 2867	. . . 4 $/\$ $/\$ $/\$ $/\$
50	16, 49	anim12d 563	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		xmetres 20993	. . . 4
52		iscau2 21842	. . . 4 $/\$ $/\$ $/\$
53	51, 52	syl 16	. . 3 $/\$ $/\$ $/\$
54		iscau2 21842	. . 3 $/\$ $/\$ $/\$
55	50, 53, 54	3imtr4d 268	. 2
56	55	ssrdv 3505	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wcel 1819

wral 2807

wrex 2808

cvv 3109

cin 3470

wss 3471 class class class wbr 4456

cxp 5006

cdm 5008

cres 5010

wfun 5588

cfv 5594 (class class class)co 6296

cpm 7439

cc 9507

clt 9645

cz 10885

cuz 11106

crp 11245

cxmt 18530

cca 21818

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-po 4809 df-so 4810 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 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-ov 6299 df-oprab 6300 df-mpt2 6301 df-1st 6799 df-2nd 6800 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-neg 9827 df-z 10886 df-uz 11107 df-rp 11246 df-xadd 11344 df-psmet 18538 df-xmet 18539 df-bl 18541 df-cau 21821

This theorem is referenced by: (None)

W3C validator