Theorem lmfval 7922

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 3265	. . . 4 |- ((P~(CC X. X) e. V /\ X e. V) -> (P~(CC X. X) X. X) e. V)
2		dmexg 3364	. . . . . . 7 |- (D e. Met -> dom D e. V)
3		dmexg 3364	. . . . . . 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 1555	. . . . 5 |- (D e. Met -> X e. V)
7		axcnex 5279	. . . . . 6 |- CC e. V
8		xpexg 3265	. . . . . 6 |- ((CC e. V /\ X e. V) -> (CC X. X) e. V)
9	7, 8	mpan 697	. . . . 5 |- (X e. V -> (CC X. X) e. V)
10		pwexg 2752	. . . . 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 473	. . 3 |- (D e. Met -> (P~(CC X. X) X. X) e. V)
13		df-3an 779	. . . . . . 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 1816	. . . . . . . . 9 |- f e. V
15	14	elpw 2408	. . . . . . . 8 |- (f e. P~(CC X. X) <-> f (_ (CC X. X))
16	15	3anbi1i 826	. . . . . . 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 2676	. . . . 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 3240	. . . . 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 2095	. . . 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 2726	. . . 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 697	. . 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 3317	. . . . . . . . 9 |- (z = D -> dom z = dom D)
25	24	dmeqd 3319	. . . . . . . 8 |- (z = D -> dom dom z = dom dom D)
26	25, 5	syl6eqr 1528	. . . . . . 7 |- (z = D -> dom dom z = X)
27		xpeq2 3207	. . . . . . 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 2092	. . . . 5 |- (z = D -> (f (_ (CC X. dom dom z) <-> f (_ (CC X. X)))
30	26	eleq2d 1544	. . . . 5 |- (z = D -> (y e. dom dom z <-> y e. X))
31	26	eleq2d 1544	. . . . . . . . . 10 |- (z = D -> ((f` k) e. dom dom z <-> (f` k) e. X))
32	31	anbi1d 619	. . . . . . . . 9 |- (z = D -> (((f` k) e. dom dom z /\ ((f` k)Dy) < x) <-> ((f` k) e. X /\ ((f` k)Dy) < x)))
33	32	imbi2d 614	. . . . . . . 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 1685	. . . . . . 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 614	. . . . . 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 1666	. . . . 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 895	. . . 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 2675	. . 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)