Theorem metcnpi3 7889

Description: Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 7888 with non-strict ordering.

Hypotheses

Ref	Expression
metcn.1	|- X = dom dom C
metcn.2	|- J = (Open` C)
metcn.3	|- Y = dom dom D
metcn.4	|- K = (Open` D)

Assertion

Ref	Expression
metcnpi3	|- (((C e. Met /\ D e. Met /\ P e. X) /\ (F e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.x e. RR (0 < x /\ A.y e. X ((yCP) <_ x -> ((F` y)D(F` P)) <_ A)))

Distinct variable groups:   x,y,F   x,C,y   x,D,y   x,X,y   x,Y,y   x,P,y   x,J,y   x,K,y   x,A,y

Proof of Theorem metcnpi3

Step	Hyp	Ref	Expression
1		metcn.1	. . 3 |- X = dom dom C
2		metcn.2	. . 3 |- J = (Open` C)
3		metcn.3	. . 3 |- Y = dom dom D
4		metcn.4	. . 3 |- K = (Open` D)
5	1, 2, 3, 4	metcnpi2 7888	. 2 |- (((C e. Met /\ D e. Met /\ P e. X) /\ (F e. ((J CnP K)` P) /\ A e. RR /\ 0 < A)) -> E.z e. RR (0 < z /\ A.y e. X ((yCP) < z -> ((F` y)D(F` P)) < A)))
6	1, 3, 2, 4	metcnpf 7880	. . . . 5 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F e. ((J CnP K)` P)) -> F:X-->Y)
7		breq2 2628	. . . . . . . . . . 11 |- (x = (z / 2) -> (0 < x <-> 0 < (z / 2)))
8		breq2 2628	. . . . . . . . . . . . 13 |- (x = (z / 2) -> ((yCP) <_ x <-> (yCP) <_ (z / 2)))
9	8	imbi1d 615	. . . . . . . . . . . 12 |- (x = (z / 2) -> (((yCP) <_ x -> ((F` y)D(F` P)) <_ A) <-> ((yCP) <_ (z / 2) -> ((F` y)D(F` P)) <_ A)))
10	9	ralbidv 1666	. . . . . . . . . . 11 |- (x = (z / 2) -> (A.y e. X ((yCP) <_ x -> ((F` y)D(F` P)) <_ A) <-> A.y e. X ((yCP) <_ (z / 2) -> ((F` y)D(F` P)) <_ A)))
11	7, 10	anbi12d 630	. . . . . . . . . 10 |- (x = (z / 2) -> ((0 < x /\ A.y e. X ((yCP) <_ x -> ((F` y)D(F` P)) <_ A)) <-> (0 < (z / 2) /\ A.y e. X ((yCP) <_ (z / 2) -> ((F` y)D(F` P)) <_ A))))
12	11	rcla4ev 1880	. . . . . . . . 9 |- (((z / 2) e. RR /\ (0 < (z / 2) /\ A.y e. X ((yCP) <_ (z / 2) -> ((F` y)D(F` P)) <_ A))) -> E.x e. RR (0 < x /\ A.y e. X ((yCP) <_ x -> ((F` y)D(F` P)) <_ A)))
13		rehalfclt 6036	. . . . . . . . . 10 |- (z e. RR -> (z / 2) e. RR)
14	13	ad2antrl 408	. . . . . . . . 9 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ (0 < z /\ A.y e. X ((yCP) < z -> ((F` y)D(F` P)) < A)))) -> (z / 2) e. RR)
15	1	metcl 7808	. . . . . . . . . . . . . . . . . . . . 21 |- ((C e. Met /\ y e. X /\ P e. X) -> (yCP) e. RR)
16	15	3com23 841	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. Met /\ P e. X /\ y e. X) -> (yCP) e. RR)
17		halfpost 6038	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. RR -> (0 < z <-> (z / 2) < z))
18	17	biimpa 418	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ 0 < z) -> (z / 2) < z)
19	18	adantl 390	. . . . . . . . . . . . . . . . . . . . . 22 |- (((yCP) e. RR /\ (z e. RR /\ 0 < z)) -> (z / 2) < z)
20		lelttrt 5535	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((yCP) e. RR /\ (z / 2) e. RR /\ z e. RR) -> (((yCP) <_ (z / 2) /\ (z / 2) < z) -> (yCP) < z))
21		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((yCP) e. RR /\ z e. RR) -> (yCP) e. RR)
22	13	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((yCP) e. RR /\ z e. RR) -> (z / 2) e. RR)
23		pm3.27 323	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((yCP) e. RR /\ z e. RR) -> z e. RR)
24	20, 21, 22, 23	syl3anc 860	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((yCP) e. RR /\ z e. RR) -> (((yCP) <_ (z / 2) /\ (z / 2) < z) -> (yCP) < z))
25	24	adantrr 397	. . . . . . . . . . . . . . . . . . . . . 22 |- (((yCP) e. RR /\ (z e. RR /\ 0 < z)) -> (((yCP) <_ (z / 2) /\ (z / 2) < z) -> (yCP) < z))
26	19, 25	mpan2d 704	. . . . . . . . . . . . . . . . . . . . 21 |- (((yCP) e. RR /\ (z e. RR /\ 0 < z)) -> ((yCP) <_ (z / 2) -> (yCP) < z))
27	26	ex 373	. . . . . . . . . . . . . . . . . . . 20 |- ((yCP) e. RR -> ((z e. RR /\ 0 < z) -> ((yCP) <_ (z / 2) -> (yCP) < z)))
28	16, 27	syl 10	. . . . . . . . . . . . . . . . . . 19 |- ((C e. Met /\ P e. X /\ y e. X) -> ((z e. RR /\ 0 < z) -> ((yCP) <_ (z / 2) -> (yCP) < z)))
29	28	3expia 837	. . . . . . . . . . . . . . . . . 18 |- ((C e. Met /\ P e. X) -> (y e. X -> ((z e. RR /\ 0 < z) -> ((yCP) <_ (z / 2) -> (yCP) < z))))
30	29	com23 32	. . . . . . . . . . . . . . . . 17 |- ((C e. Met /\ P e. X) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((yCP) <_ (z / 2) -> (yCP) < z))))
31	30	3adant2 800	. . . . . . . . . . . . . . . 16 |- ((C e. Met /\ D e. Met /\ P e. X) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((yCP) <_ (z / 2) -> (yCP) < z))))
32	31	ad2antrr 406	. . . . . . . . . . . . . . 15 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((yCP) <_ (z / 2) -> (yCP) < z))))
33	32	imp31 362	. . . . . . . . . . . . . 14 |- ((((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) /\ y e. X) -> ((yCP) <_ (z / 2) -> (yCP) < z))
34		ltlet 5532	. . . . . . . . . . . . . . . 16 |- ((((F` y)D(F` P)) e. RR /\ A e. RR) -> (((F` y)D(F` P)) < A -> ((F` y)D(F` P)) <_ A))
35	3	metcl 7808	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ (F` y) e. Y /\ (F` P) e. Y) -> ((F` y)D(F` P)) e. RR)
36	35	3expb 836	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((D e. Met /\ ((F` y) e. Y /\ (F` P) e. Y)) -> ((F` y)D(F` P)) e. RR)
37		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F:X-->Y /\ y e. X) -> (F` y) e. Y)
38		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F:X-->Y /\ P e. X) -> (F` P) e. Y)
39	37, 38	anim12i 333	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F:X-->Y /\ y e. X) /\ (F:X-->Y /\ P e. X)) -> ((F` y) e. Y /\ (F` P) e. Y))
40	39	anandis 514	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:X-->Y /\ (y e. X /\ P e. X)) -> ((F` y) e. Y /\ (F` P) e. Y))
41	40	ancom2s 489	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->Y /\ (P e. X /\ y e. X)) -> ((F` y) e. Y /\ (F` P) e. Y))
42	36, 41	sylan2 453	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D e. Met /\ (F:X-->Y /\ (P e. X /\ y e. X))) -> ((F` y)D(F` P)) e. RR)
43	42	exp45 388	. . . . . . . . . . . . . . . . . . . . 21 |- (D e. Met -> (F:X-->Y -> (P e. X -> (y e. X -> ((F` y)D(F` P)) e. RR))))
44	43	com23 32	. . . . . . . . . . . . . . . . . . . 20 |- (D e. Met -> (P e. X -> (F:X-->Y -> (y e. X -> ((F` y)D(F` P)) e. RR))))
45	44	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((D e. Met /\ P e. X) -> (F:X-->Y -> (y e. X -> ((F` y)D(F` P)) e. RR)))
46	45	3adant1 799	. . . . . . . . . . . . . . . . . 18 |- ((C e. Met /\ D e. Met /\ P e. X) -> (F:X-->Y -> (y e. X -> ((F` y)D(F` P)) e. RR)))
47	46	imp31 362	. . . . . . . . . . . . . . . . 17 |- ((((C