caussi - Metamath Proof Explorer

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

Theorem caussi 20650

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 3558	. . . . . . . . 9
2		xpss2 4936	. . . . . . . . 9
3	1, 2	ax-mp 5	. . . . . . . 8
4		sstr 3352	. . . . . . . 8 $/\$
5	3, 4	mpan2 664	. . . . . . 7
6	5	anim2i 564	. . . . . 6 $/\$ $/\$
7	6	a1i 11	. . . . 5 $/\$ $/\$
8		elfvdm 5704	. . . . . . 7
9		inex1g 4423	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11		cnex 9351	. . . . . 6
12		elpmg 7216	. . . . . 6 $/\$ $/\$
13	10, 11, 12	sylancl 655	. . . . 5 $/\$
14		elpmg 7216	. . . . . 6 $/\$ $/\$
15	8, 11, 14	sylancl 655	. . . . 5 $/\$
16	7, 13, 15	3imtr4d 268	. . . 4
17		uzid 10863	. . . . . . . . . 10
18	17	adantl 463	. . . . . . . . 9 $/\$
19		simp2 982	. . . . . . . . . 10 $/\$ $/\$
20	19	ralimi 2781	. . . . . . . . 9 $/\$ $/\$
21		fveq2 5679	. . . . . . . . . . 11
22	21	eleq1d 2499	. . . . . . . . . 10
23	22	rspcva 3060	. . . . . . . . 9 $/\$
24	18, 20, 23	syl2an 474	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
25		inss2 3559	. . . . . . . . . . . . . 14
26		simpr 458	. . . . . . . . . . . . . 14 $/\$ $/\$
27	25, 26	sseldi 3342	. . . . . . . . . . . . 13 $/\$ $/\$
28	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
29	28	sselda 3344	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
30		simplr 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
31	29, 30	ovresd 6220	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
32	31	breq1d 4290	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	32	biimpd 207	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
34	33	imdistanda 686	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
35	1	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
36	35	sseld 3343	. . . . . . . . . . . . . . 15 $/\$ $/\$
37	36	anim1d 559	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
38	34, 37	syld 44	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
39	27, 38	syldan 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
40	39	anim2d 560	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41		3anass 962	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
42		3anass 962	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
43	40, 41, 42	3imtr4g 270	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	43	ralimdv 2785	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45	44	impancom 438	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	24, 45	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	ex 434	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
48	47	reximdva 2818	. . . . 5 $/\$ $/\$ $/\$ $/\$
49	48	ralimdv 2785	. . . 4 $/\$ $/\$ $/\$ $/\$
50	16, 49	anim12d 558	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51		xmetres 19781	. . . 4
52		iscau2 20630	. . . 4 $/\$ $/\$ $/\$
53	51, 52	syl 16	. . 3 $/\$ $/\$ $/\$
54		iscau2 20630	. . 3 $/\$ $/\$ $/\$
55	50, 53, 54	3imtr4d 268	. 2
56	55	ssrdv 3350	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wcel 1755

wral 2705

wrex 2706

cvv 2962

cin 3315

wss 3316 class class class wbr 4280

cxp 4825

cdm 4827

cres 4829

wfun 5400

cfv 5406 (class class class)co 6080

cpm 7203

cc 9268

clt 9406

cz 10634

cuz 10849

crp 10979

cxmt 17645

cca 20606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-op 3872 df-uni 4080 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-id 4623 df-po 4628 df-so 4629 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-1st 6566 df-2nd 6567 df-er 7089 df-map 7204 df-pm 7205 df-en 7299 df-dom 7300 df-sdom 7301 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-neg 9586 df-z 10635 df-uz 10850 df-rp 10980 df-xadd 11078 df-psmet 17653 df-xmet 17654 df-bl 17656 df-cau 20609

This theorem is referenced by: (None)

W3C validator