Theorem lmbr 7928

Description: Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition F (_ (CC X. X) allows us to use objects more general than sequences when convenient; see the comment in df-lm 7922.

Hypothesis

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

Assertion

Ref	Expression
lmbr	|- ((D e. Met /\ P e. A) -> (F(~~>m` D)P <-> (F (_ (CC X. X) /\ P e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < x))))))

Distinct variable groups:   j,k,x,F   D,j,k,x   P,j,k,x

Proof of Theorem lmbr

Step	Hyp	Ref	Expression
1		simpll 412	. . 3 |- (((D e. Met /\ P e. A) /\ F(~~>m` D)P) -> D e. Met)
2		brrelex 3207	. . . . . 6 |- ((Rel (~~>m` D) /\ F(~~>m` D)P) -> F e. V)
3		lmrel 7927	. . . . . 6 |- (D e. Met -> Rel (~~>m` D))
4	2, 3	sylan 448	. . . . 5 |- ((D e. Met /\ F(~~>m` D)P) -> F e. V)
5	4	anim1i 334	. . . 4 |- (((D e. Met /\ F(~~>m` D)P) /\ P e. A) -> (F e. V /\ P e. A))
6	5	an1rs 489	. . 3 |- (((D e. Met /\ P e. A) /\ F(~~>m` D)P) -> (F e. V /\ P e. A))
7	1, 6	jca 288	. 2 |- (((D e. Met /\ P e. A) /\ F(~~>m` D)P) -> (D e. Met /\ (F e. V /\ P e. A)))
8		pm3.26 319	. . . . 5 |- ((D e. Met /\ (P e. A /\ F (_ (CC X. X))) -> D e. Met)
9		ssexg 2721	. . . . . . . . 9 |- ((F (_ (CC X. X) /\ (CC X. X) e. V) -> F e. V)
10		dmexg 3358	. . . . . . . . . . . 12 |- (D e. Met -> dom D e. V)
11		dmexg 3358	. . . . . . . . . . . 12 |- (dom D e. V -> dom dom D e. V)
12	10, 11	syl 10	. . . . . . . . . . 11 |- (D e. Met -> dom dom D e. V)
13		lmbr.1	. . . . . . . . . . 11 |- X = dom dom D
14	12, 13	syl5eqel 1552	. . . . . . . . . 10 |- (D e. Met -> X e. V)
15		axcnex 5267	. . . . . . . . . . 11 |- CC e. V
16		xpexg 3259	. . . . . . . . . . 11 |- ((CC e. V /\ X e. V) -> (CC X. X) e. V)
17	15, 16	mpan 695	. . . . . . . . . 10 |- (X e. V -> (CC X. X) e. V)
18	14, 17	syl 10	. . . . . . . . 9 |- (D e. Met -> (CC X. X) e. V)
19	9, 18	sylan2 451	. . . . . . . 8 |- ((F (_ (CC X. X) /\ D e. Met) -> F e. V)
20	19	ancoms 436	. . . . . . 7 |- ((D e. Met /\ F (_ (CC X. X)) -> F e. V)
21	20	adantrl 394	. . . . . 6 |- ((D e. Met /\ (P e. A /\ F (_ (CC X. X))) -> F e. V)
22		simprl 414	. . . . . 6 |- ((D e. Met /\ (P e. A /\ F (_ (CC X. X))) -> P e. A)
23	21, 22	jca 288	. . . . 5 |- ((D e. Met /\ (P e. A /\ F (_ (CC X. X))) -> (F e. V /\ P e. A))
24	8, 23	jca 288	. . . 4 |- ((D e. Met /\ (P e. A /\ F (_ (CC X. X))) -> (D e. Met /\ (F e. V /\ P e. A)))
25	24	anassrs 441	. . 3 |- (((D e. Met /\ P e. A) /\ F (_ (CC X. X)) -> (D e. Met /\ (F e. V /\ P e. A)))
26	25	3ad2antr1 812	. 2 |- (((D e. Met /\ P e. A) /\ (F (_ (CC X. X) /\ P e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < x))))) -> (D e. Met /\ (F e. V /\ P e. A)))
27	13	lmfval 7925	. . . 4 |- (D e. Met -> (~~>m` D) = {<.z, w>. | (z (_ (CC X. X) /\ w e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x))))})
28		breq 2621	. . . 4 |- ((~~>m` D) = {<.z, w>. | (z (_ (CC X. X) /\ w e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x))))} -> (F(~~>m` D)P <-> F{<.z, w>. | (z (_ (CC X. X) /\ w e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x))))}P))
29	27, 28	syl 10	. . 3 |- (D e. Met -> (F(~~>m` D)P <-> F{<.z, w>. | (z (_ (CC X. X) /\ w e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x))))}P))
30		sseq1 2082	. . . . 5 |- (z = F -> (z (_ (CC X. X) <-> F (_ (CC X. X)))
31		fveq1 3723	. . . . . . . . . . 11 |- (z = F -> (z` k) = (F` k))
32	31	eleq1d 1540	. . . . . . . . . 10 |- (z = F -> ((z` k) e. X <-> (F` k) e. X))
33	31	opreq1d 3975	. . . . . . . . . . 11 |- (z = F -> ((z` k)Dw) = ((F` k)Dw))
34	33	breq1d 2629	. . . . . . . . . 10 |- (z = F -> (((z` k)Dw) < x <-> ((F` k)Dw) < x))
35	32, 34	anbi12d 628	. . . . . . . . 9 |- (z = F -> (((z` k) e. X /\ ((z` k)Dw) < x) <-> ((F` k) e. X /\ ((F` k)Dw) < x)))
36	35	imbi2d 612	. . . . . . . 8 |- (z = F -> ((j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x)) <-> (j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x))))
37	36	rexralbidv 1682	. . . . . . 7 |- (z = F -> (E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x)) <-> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x))))
38	37	imbi2d 612	. . . . . 6 |- (z = F -> ((0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x))) <-> (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x)))))
39	38	ralbidv 1663	. . . . 5 |- (z = F -> (A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x))) <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x)))))
40	30, 39	3anbi13d 895	. . . 4 |- (z = F -> ((z (_ (CC X. X) /\ w e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((z` k) e. X /\ ((z` k)Dw) < x)))) <-> (F (_ (CC X. X) /\ w e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x))))))
41		eleq1 1534	. . . . 5 |- (w = P -> (w e. X <-> P e. X))
42		opreq2 3969	. . . . . . . . . . 11 |- (w = P -> ((F` k)Dw) = ((F` k)DP))
43	42	breq1d 2629	. . . . . . . . . 10 |- (w = P -> (((F` k)Dw) < x <-> ((F` k)DP) < x))
44	43	anbi2d 616	. . . . . . . . 9 |- (w = P -> (((F` k) e. X /\ ((F` k)Dw) < x) <-> ((F` k) e. X /\ ((F` k)DP) < x)))
45	44	imbi2d 612	. . . . . . . 8 |- (w = P -> ((j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x)) <-> (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < x))))
46	45	rexralbidv 1682	. . . . . . 7 |- (w = P -> (E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x)) <-> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < x))))
47	46	imbi2d 612	. . . . . 6 |- (w = P -> ((0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)Dw) < x))) <-> (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((F` k) e. X /\ ((F` k)DP) < x)))))
48	47	ralbidv 1663	. . . . 5 |- (w = P -> (A.x e. RR (