Theorem lmfval 7877

Description: The relation "sequence f converges to point y" in a metric space.

Hypothesis

Ref	Expression
lmfval.1	|- X = dom dom D

Assertion

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

Distinct variable groups:   f,j,k,x,y,D   f,X,y

Proof of Theorem lmfval

Step	Hyp	Ref	Expression
1		xpexg 3254	. . . 4 |- ((P~(CC X. X) e. V /\ X e. V) -> (P~(CC X. X) X. X) e. V)
2		dmexg 3352	. . . . . . 7 |- (D e. Met -> dom D e. V)
3		dmexg 3352	. . . . . . 7 |- (dom D e. V -> dom dom D e. V)
4	2, 3	syl 10	. . . . . 6 |- (D e. Met -> dom dom D e. V)
5		lmfval.1	. . . . . 6 |- X = dom dom D
6	4, 5	syl5eqel 1549	. . . . 5 |- (D e. Met -> X e. V)
7		axcnex 5247	. . . . . 6 |- CC e. V
8		xpexg 3254	. . . . . 6 |- ((CC e. V /\ X e. V) -> (CC X. X) e. V)
9	7, 8	mpan 694	. . . . 5 |- (X e. V -> (CC X. X) e. V)
10		pwexg 2741	. . . . 5 |- ((CC X. X) e. V -> P~(CC X. X) e. V)
11	6, 9, 10	3syl 20	. . . 4 |- (D e. Met -> P~(CC X. X) e. V)
12	1, 11, 6	sylanc 471	. . 3 |- (D e. Met -> (P~(CC X. X) X. X) e. V)
13		df-3an 776	. . . . . . 7 |- ((f e. P~(CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))) <-> ((f e. P~(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
14		visset 1809	. . . . . . . . 9 |- f e. V
15	14	elpw 2400	. . . . . . . 8 |- (f e. P~(CC X. X) <-> f (_ (CC X. X))
16	15	3anbi1i 823	. . . . . . 7 |- ((f e. P~(CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))) <-> (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
17	13, 16	bitr3 175	. . . . . 6 |- (((f e. P~(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))) <-> (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
18	17	opabbii 2666	. . . . 5 |- {<.f, y>. | ((f e. P~(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} = {<.f, y>. | (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))}
19		opabssxp 3229	. . . . 5 |- {<.f, y>. | ((f e. P~(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} (_ (P~(CC X. X) X. X)
20	18, 19	eqsstr3 2088	. . . 4 |- {<.f, y>. | (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} (_ (P~(CC X. X) X. X)
21		ssexg 2716	. . . 4 |- (({<.f, y>. | (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} (_ (P~(CC X. X) X. X) /\ (P~(CC X. X) X. X) e. V) -> {<.f, y>. | (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} e. V)
22	20, 21	mpan 694	. . 3 |- ((P~(CC X. X) X. X) e. V -> {<.f, y>. | (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} e. V)
23	12, 22	syl 10	. 2 |- (D e. Met -> {<.f, y>. | (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} e. V)
24		dmeq 3306	. . . . . . . . 9 |- (z = D -> dom z = dom D)
25	24	dmeqd 3308	. . . . . . . 8 |- (z = D -> dom dom z = dom dom D)
26	25, 5	syl6eqr 1522	. . . . . . 7 |- (z = D -> dom dom z = X)
27		xpeq2 3196	. . . . . . 7 |- (dom dom z = X -> (CC X. dom dom z) = (CC X. X))
28	26, 27	syl 10	. . . . . 6 |- (z = D -> (CC X. dom dom z) = (CC X. X))
29	28	sseq2d 2085	. . . . 5 |- (z = D -> (f (_ (CC X. dom dom z) <-> f (_ (CC X. X)))
30	26	eleq2d 1538	. . . . 5 |- (z = D -> (y e. dom dom z <-> y e. X))
31	26	eleq2d 1538	. . . . . . . . . 10 |- (z = D -> ((f` k) e. dom dom z <-> (f` k) e. X))
32	31	anbi1d 616	. . . . . . . . 9 |- (z = D -> (((f` k) e. dom dom z /\ ((f` k)Dy) < x) <-> ((f` k) e. X /\ ((f` k)Dy) < x)))
33	32	imbi2d 611	. . . . . . . 8 |- (z = D -> ((j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x)) <-> (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))
34	33	rexralbidv 1679	. . . . . . 7 |- (z = D -> (E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x)) <-> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))
35	34	imbi2d 611	. . . . . 6 |- (z = D -> ((0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))) <-> (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
36	35	ralbidv 1660	. . . . 5 |- (z = D -> (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))) <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
37	29, 30, 36	3anbi123d 891	. . . 4 |- (z = D -> ((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)))) <-> (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))))
38	37	opabbidv 2665	. . 3 |- (z = D -> {<.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))))} = {<.f, y>. | (f (_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e.