caussi - Metamath Proof Explorer

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

Theorem caussi 20788

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 3565	. . . . . . . . 9
2		xpss2 4944	. . . . . . . . 9
3	1, 2	ax-mp 5	. . . . . . . 8
4		sstr 3359	. . . . . . . 8 $/\$
5	3, 4	mpan2 671	. . . . . . 7
6	5	anim2i 569	. . . . . 6 $/\$ $/\$
7	6	a1i 11	. . . . 5 $/\$ $/\$
8		elfvdm 5711	. . . . . . 7
9		inex1g 4430	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11		cnex 9355	. . . . . 6
12		elpmg 7220	. . . . . 6 $/\$ $/\$
13	10, 11, 12	sylancl 662	. . . . 5 $/\$
14		elpmg 7220	. . . . . 6 $/\$ $/\$
15	8, 11, 14	sylancl 662	. . . . 5 $/\$
16	7, 13, 15	3imtr4d 268	. . . 4
17		uzid 10867	. . . . . . . . . 10
18	17	adantl 466	. . . . . . . . 9 $/\$
19		simp2 989	. . . . . . . . . 10 $/\$ $/\$
20	19	ralimi 2786	. . . . . . . . 9 $/\$ $/\$
21		fveq2 5686	. . . . . . . . . . 11
22	21	eleq1d 2504	. . . . . . . . . 10
23	22	rspcva 3066	. . . . . . . . 9 $/\$
24	18, 20, 23	syl2an 477	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25		inss2 3566	. . . . . . . . . . . . . 14
26		simpr 461	. . . . . . . . . . . . . 14 $/\$ $/\$
27	25, 26	sseldi 3349	. . . . . . . . . . . . 13 $/\$ $/\$
28	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
29	28	sselda 3351	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
30		simplr 754	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
31	29, 30	ovresd 6226	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
32	31	breq1d 4297	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	32	biimpd 207	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34	33	imdistanda 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
35	1	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
36	35	sseld 3350	. . . . . . . . . . . . . . 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 2790	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	44	impancom 440	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	24, 45	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
48	47	reximdva 2823	. . . . 5 $/\$ $/\$ $/\$ $/\$
49	48	ralimdv 2790	. . . 4 $/\$ $/\$ $/\$ $/\$
50	16, 49	anim12d 563	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		xmetres 19919	. . . 4
52		iscau2 20768	. . . 4 $/\$ $/\$ $/\$
53	51, 52	syl 16	. . 3 $/\$ $/\$ $/\$
54		iscau2 20768	. . 3 $/\$ $/\$ $/\$
55	50, 53, 54	3imtr4d 268	. 2
56	55	ssrdv 3357	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wcel 1756

wral 2710

wrex 2711

cvv 2967

cin 3322

wss 3323 class class class wbr 4287

cxp 4833

cdm 4835

cres 4837

wfun 5407

cfv 5413 (class class class)co 6086

cpm 7207

cc 9272

clt 9410

cz 10638

cuz 10853

crp 10983

cxmt 17781

cca 20744

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-po 4636 df-so 4637 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-1st 6572 df-2nd 6573 df-er 7093 df-map 7208 df-pm 7209 df-en 7303 df-dom 7304 df-sdom 7305 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-neg 9590 df-z 10639 df-uz 10854 df-rp 10984 df-xadd 11082 df-psmet 17789 df-xmet 17790 df-bl 17792 df-cau 20747

This theorem is referenced by: (None)

W3C validator