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 22260

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 3651	. . . . . . . . 9
2		xpss2 4943	. . . . . . . . 9
3	1, 2	ax-mp 5	. . . . . . . 8
4		sstr 3439	. . . . . . . 8 $/\$
5	3, 4	mpan2 676	. . . . . . 7
6	5	anim2i 572	. . . . . 6 $/\$ $/\$
7	6	a1i 11	. . . . 5 $/\$ $/\$
8		elfvdm 5889	. . . . . . 7
9		inex1g 4545	. . . . . . 7
10	8, 9	syl 17	. . . . . 6
11		cnex 9617	. . . . . 6
12		elpmg 7484	. . . . . 6 $/\$ $/\$
13	10, 11, 12	sylancl 667	. . . . 5 $/\$
14		elpmg 7484	. . . . . 6 $/\$ $/\$
15	8, 11, 14	sylancl 667	. . . . 5 $/\$
16	7, 13, 15	3imtr4d 272	. . . 4
17		uzid 11170	. . . . . . . . . 10
18	17	adantl 468	. . . . . . . . 9 $/\$
19		simp2 1008	. . . . . . . . . 10 $/\$ $/\$
20	19	ralimi 2780	. . . . . . . . 9 $/\$ $/\$
21		fveq2 5863	. . . . . . . . . . 11
22	21	eleq1d 2512	. . . . . . . . . 10
23	22	rspcva 3147	. . . . . . . . 9 $/\$
24	18, 20, 23	syl2an 480	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25		inss2 3652	. . . . . . . . . . . . . 14
26		simpr 463	. . . . . . . . . . . . . 14 $/\$ $/\$
27	25, 26	sseldi 3429	. . . . . . . . . . . . 13 $/\$ $/\$
28	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
29	28	sselda 3431	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
30		simplr 761	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
31	29, 30	ovresd 6434	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
32	31	breq1d 4411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	32	biimpd 211	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34	33	imdistanda 698	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
35	1	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
36	35	sseld 3430	. . . . . . . . . . . . . . 15 $/\$ $/\$
37	36	anim1d 567	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
38	34, 37	syld 45	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
39	27, 38	syldan 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40	39	anim2d 568	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		3anass 988	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42		3anass 988	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	40, 41, 42	3imtr4g 274	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	43	ralimdv 2797	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	44	impancom 442	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	24, 45	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	ex 436	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
48	47	reximdva 2861	. . . . 5 $/\$ $/\$ $/\$ $/\$
49	48	ralimdv 2797	. . . 4 $/\$ $/\$ $/\$ $/\$
50	16, 49	anim12d 566	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		xmetres 21372	. . . 4
52		iscau2 22240	. . . 4 $/\$ $/\$ $/\$
53	51, 52	syl 17	. . 3 $/\$ $/\$ $/\$
54		iscau2 22240	. . 3 $/\$ $/\$ $/\$
55	50, 53, 54	3imtr4d 272	. 2
56	55	ssrdv 3437	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 984

wcel 1886

wral 2736

wrex 2737

cvv 3044

cin 3402

wss 3403 class class class wbr 4401

cxp 4831

cdm 4833

cres 4835

wfun 5575

cfv 5581 (class class class)co 6288

cpm 7470

cc 9534

clt 9672

cz 10934

cuz 11156

crp 11299

cxmt 18948

cca 22216

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-id 4748 df-po 4754 df-so 4755 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-1st 6790 df-2nd 6791 df-er 7360 df-map 7471 df-pm 7472 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-neg 9860 df-z 10935 df-uz 11157 df-rp 11300 df-xadd 11407 df-psmet 18955 df-xmet 18956 df-bl 18958 df-cau 22219

This theorem is referenced by: (None)

W3C validator