causs - Metamath Proof Explorer

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

Theorem causs 22317

Description: Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)

**Assertion**
Ref	Expression
causs	$/\$

Proof of Theorem causs Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		caufpm 22301	. . . . . . . . 9 $/\$
2		elfvdm 5914	. . . . . . . . . . 11
3		cnex 9646	. . . . . . . . . . 11
4		elpmg 7513	. . . . . . . . . . 11 $/\$ $/\$
5	2, 3, 4	sylancl 673	. . . . . . . . . 10 $/\$
6	5	biimpa 491	. . . . . . . . 9 $/\$ $/\$
7	1, 6	syldan 477	. . . . . . . 8 $/\$ $/\$
8	7	simprd 469	. . . . . . 7 $/\$
9		rnss 5082	. . . . . . 7
10	8, 9	syl 17	. . . . . 6 $/\$
11		rnxpss 5288	. . . . . 6
12	10, 11	syl6ss 3456	. . . . 5 $/\$
13	12	adantlr 726	. . . 4 $/\$ $/\$
14		frn 5758	. . . . 5
15	14	ad2antlr 738	. . . 4 $/\$ $/\$
16	13, 15	ssind 3668	. . 3 $/\$ $/\$
17	16	ex 440	. 2 $/\$
18		xmetres 21428	. . . . . . . . 9
19		caufpm 22301	. . . . . . . . 9 $/\$
20	18, 19	sylan 478	. . . . . . . 8 $/\$
21		inex1g 4560	. . . . . . . . . . 11
22	2, 21	syl 17	. . . . . . . . . 10
23		elpmg 7513	. . . . . . . . . 10 $/\$ $/\$
24	22, 3, 23	sylancl 673	. . . . . . . . 9 $/\$
25	24	biimpa 491	. . . . . . . 8 $/\$ $/\$
26	20, 25	syldan 477	. . . . . . 7 $/\$ $/\$
27	26	simprd 469	. . . . . 6 $/\$
28		rnss 5082	. . . . . 6
29	27, 28	syl 17	. . . . 5 $/\$
30		rnxpss 5288	. . . . 5
31	29, 30	syl6ss 3456	. . . 4 $/\$
32	31	ex 440	. . 3
33	32	adantr 471	. 2 $/\$
34		ffn 5751	. . . 4
35		df-f 5605	. . . . 5 $/\$
36	35	simplbi2 635	. . . 4
37	34, 36	syl 17	. . 3
38		inss2 3665	. . . . . . . . 9
39	38	a1i 11	. . . . . . . 8
40		fss 5760	. . . . . . . 8 $/\$
41	39, 40	sylan2 481	. . . . . . 7 $/\$
42	41	ancoms 459	. . . . . 6 $/\$
43		ffvelrn 6043	. . . . . . . . . . . 12 $/\$
44	43	adantr 471	. . . . . . . . . . 11 $/\$ $/\$
45		eluznn 11258	. . . . . . . . . . . . 13 $/\$
46		ffvelrn 6043	. . . . . . . . . . . . 13 $/\$
47	45, 46	sylan2 481	. . . . . . . . . . . 12 $/\$ $/\$
48	47	anassrs 658	. . . . . . . . . . 11 $/\$ $/\$
49	44, 48	ovresd 6464	. . . . . . . . . 10 $/\$ $/\$
50	49	breq1d 4426	. . . . . . . . 9 $/\$ $/\$
51	50	ralbidva 2836	. . . . . . . 8 $/\$
52	51	rexbidva 2910	. . . . . . 7
53	52	ralbidv 2839	. . . . . 6
54	42, 53	syl 17	. . . . 5 $/\$
55		nnuz 11223	. . . . . 6
56	18	adantr 471	. . . . . 6 $/\$
57		1zzd 10997	. . . . . 6 $/\$
58		eqidd 2463	. . . . . 6 $/\$ $/\$
59		eqidd 2463	. . . . . 6 $/\$ $/\$
60		simpr 467	. . . . . 6 $/\$
61	55, 56, 57, 58, 59, 60	iscauf 22299	. . . . 5 $/\$
62		simpl 463	. . . . . 6 $/\$
63		id 22	. . . . . . 7
64		inss1 3664	. . . . . . . 8
65	64	a1i 11	. . . . . . 7
66		fss 5760	. . . . . . 7 $/\$
67	63, 65, 66	syl2anr 485	. . . . . 6 $/\$
68	55, 62, 57, 58, 59, 67	iscauf 22299	. . . . 5 $/\$
69	54, 61, 68	3bitr4rd 294	. . . 4 $/\$
70	69	ex 440	. . 3
71	37, 70	sylan9r 668	. 2 $/\$
72	17, 33, 71	pm5.21ndd 360	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 375

wcel 1898

wral 2749

wrex 2750

cvv 3057

cin 3415

wss 3416 class class class wbr 4416

cxp 4851

cdm 4853

crn 4854

cres 4855

wfun 5595

wfn 5596

wf 5597

cfv 5601 (class class class)co 6315

cpm 7499

cc 9563

c1 9566

clt 9701

cn 10637

cuz 11188

crp 11331

cxmt 19004

cca 22272

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-cnex 9621 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 ax-pre-mulgt0 9642

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-iun 4294 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-om 6720 df-1st 6820 df-2nd 6821 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-er 7389 df-map 7500 df-pm 7501 df-en 7596 df-dom 7597 df-sdom 7598 df-pnf 9703 df-mnf 9704 df-xr 9705 df-ltxr 9706 df-le 9707 df-sub 9888 df-neg 9889 df-div 10298 df-nn 10638 df-2 10696 df-z 10967 df-uz 11189 df-rp 11332 df-xneg 11438 df-xadd 11439 df-psmet 19011 df-xmet 19012 df-bl 19014 df-cau 22275

This theorem is referenced by: minvecolem4a 26568 minvecolem4aOLD 26578 hhsscms 26979

W3C validator