df-rlim - Metamath Proof Explorer

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

Definition df-rlim 14220

Description: Define the limit relation for partial functions on the reals. See rlim 14226 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.)

**Assertion**
Ref	Expression
df-rlim	$/\$ $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-rlim**
Step	Hyp	Ref	Expression
1		crli 14216	. 2
2		vf	. . . . . . 7
3	2	cv 1482	. . . . . 6
4		cc 9934	. . . . . . 7
5		cr 9935	. . . . . . 7
6		cpm 7858	. . . . . . 7
7	4, 5, 6	co 6650	. . . . . 6
8	3, 7	wcel 1990	. . . . 5
9		vx	. . . . . . 7
10	9	cv 1482	. . . . . 6
11	10, 4	wcel 1990	. . . . 5
12	8, 11	wa 384	. . . 4 $/\$
13		vz	. . . . . . . . . 10
14	13	cv 1482	. . . . . . . . 9
15		vw	. . . . . . . . . 10
16	15	cv 1482	. . . . . . . . 9
17		cle 10075	. . . . . . . . 9
18	14, 16, 17	wbr 4653	. . . . . . . 8
19	16, 3	cfv 5888	. . . . . . . . . . 11
20		cmin 10266	. . . . . . . . . . 11
21	19, 10, 20	co 6650	. . . . . . . . . 10
22		cabs 13974	. . . . . . . . . 10
23	21, 22	cfv 5888	. . . . . . . . 9
24		vy	. . . . . . . . . 10
25	24	cv 1482	. . . . . . . . 9
26		clt 10074	. . . . . . . . 9
27	23, 25, 26	wbr 4653	. . . . . . . 8
28	18, 27	wi 4	. . . . . . 7
29	3	cdm 5114	. . . . . . 7
30	28, 15, 29	wral 2912	. . . . . 6
31	30, 13, 5	wrex 2913	. . . . 5
32		crp 11832	. . . . 5
33	31, 24, 32	wral 2912	. . . 4
34	12, 33	wa 384	. . 3 $/\$ $/\$
35	34, 2, 9	copab 4712	. 2 $/\$ $/\$
36	1, 35	wceq 1483	1 $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: rlimrel 14224 rlim 14226 rlimpm 14231

W3C validator