Definition df-lm 7919

Description: Define a function on metric spaces whose value is the convergence relation for the space. Although f is typically a function from upper integers to the metric space, it doesn't have to be. Unfortunately, the expression after "w =" must exist to use fvopab4 3786, and we use the otherwise unnecessary conjunct f (_ (CC X. dom dom z) to ensure that. This could be changed to the more liberal (but more complex) f (_ (CC X. (dom dom z u. {(/)})) if we want to allow for functions with undefined values.

Assertion

Ref	Expression
df-lm	|- ~~>m = {<.z, w>. | (z e. Met /\ w = {<.f, y>. | (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))})}

Distinct variable group:   j,k,x,y,f,z,w

Detailed syntax breakdown of Definition df-lm

Step	Hyp	Ref	Expression
1		clm 7916	. 2 class ~~>m
2		vz	. . . . . 6 set z
3	2	cv 957	. . . . 5 class z
4		cme 7786	. . . . 5 class Met
5	3, 4	wcel 960	. . . 4 wff z e. Met
6		vw	. . . . . 6 set w
7	6	cv 957	. . . . 5 class w
8		vf	. . . . . . . . 9 set f
9	8	cv 957	. . . . . . . 8 class f
10		cc 5244	. . . . . . . . 9 class CC
11	3	cdm 3176	. . . . . . . . . 10 class dom z
12	11	cdm 3176	. . . . . . . . 9 class dom dom z
13	10, 12	cxp 3174	. . . . . . . 8 class (CC X. dom dom z)
14	9, 13	wss 2050	. . . . . . 7 wff f (_ (CC X. dom dom z)
15		vy	. . . . . . . . 9 set y
16	15	cv 957	. . . . . . . 8 class y
17	16, 12	wcel 960	. . . . . . 7 wff y e. dom dom z
18		cc0 5246	. . . . . . . . . 10 class 0
19		vx	. . . . . . . . . . 11 set x
20	19	cv 957	. . . . . . . . . 10 class x
21		clt 5498	. . . . . . . . . 10 class <
22	18, 20, 21	wbr 2624	. . . . . . . . 9 wff 0 < x
23		vj	. . . . . . . . . . . . . 14 set j
24	23	cv 957	. . . . . . . . . . . . 13 class j
25		vk	. . . . . . . . . . . . . 14 set k
26	25	cv 957	. . . . . . . . . . . . 13 class k
27		cle 5307	. . . . . . . . . . . . 13 class <_
28	24, 26, 27	wbr 2624	. . . . . . . . . . . 12 wff j <_ k
29	26, 9	cfv 3188	. . . . . . . . . . . . . 14 class (f` k)
30	29, 12	wcel 960	. . . . . . . . . . . . 13 wff (f` k) e. dom dom z
31		cD	. . . . . . . . . . . . . . 15 class D
32	29, 16, 31	co 3969	. . . . . . . . . . . . . 14 class ((f` k)Dy)
33	32, 20, 21	wbr 2624	. . . . . . . . . . . . 13 wff ((f` k)Dy) < x
34	30, 33	wa 223	. . . . . . . . . . . 12 wff ((f` k) e. dom dom z /\ ((f` k)Dy) < x)
35	28, 34	wi 3	. . . . . . . . . . 11 wff (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))
36		cz 5310	. . . . . . . . . . 11 class ZZ
37	35, 25, 36	wral 1648	. . . . . . . . . 10 wff A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))
38	37, 23, 36	wrex 1649	. . . . . . . . 9 wff E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))
39	22, 38	wi 3	. . . . . . . 8 wff (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x)))
40		cr 5245	. . . . . . . 8 class RR
41	39, 19, 40	wral 1648	. . . . . . 7 wff A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x)))
42	14, 17, 41	w3a 777	. . . . . 6 wff (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))
43	42, 8, 15	copab 2671	. . . . 5 class {<.f, y>. | (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))}
44	7, 43	wceq 958	. . . 4 wff w = {<.f, y>. | (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))}
45	5, 44	wa 223	. . 3 wff (z e. Met /\ w = {<.f, y>. | (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))})
46	45, 2, 6	copab 2671	. 2 class {<.z, w>. | (z e. Met /\ w = {<.f, y>. | (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))})}
47	1, 46	wceq 958	1 wff ~~>m = {<.z, w>. | (z e. Met /\ w = {<.f, y>. | (f (_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))})}

This definition is referenced by:  lmfval 7922

Copyright terms: Public domain