Theorem metcnpi4 7893

Description: Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi 7890 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
metcnpi4	|- (((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 ((PCy) <_ x -> ((F` P)D(F` y)) <_ 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 metcnpi4

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	metcnpi 7890	. 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 ((PCy) < z -> ((F` P)D(F` y)) < A)))
6	1, 3, 2, 4	metcnpf 7883	. . . . 5 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F e. ((J CnP K)` P)) -> F:X-->Y)
7		breq2 2623	. . . . . . . . . . 11 |- (x = (z / 2) -> (0 < x <-> 0 < (z / 2)))
8		breq2 2623	. . . . . . . . . . . . 13 |- (x = (z / 2) -> ((PCy) <_ x <-> (PCy) <_ (z / 2)))
9	8	imbi1d 613	. . . . . . . . . . . 12 |- (x = (z / 2) -> (((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
10	9	ralbidv 1663	. . . . . . . . . . 11 |- (x = (z / 2) -> (A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
11	7, 10	anbi12d 628	. . . . . . . . . 10 |- (x = (z / 2) -> ((0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)) <-> (0 < (z / 2) /\ A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A))))
12	11	rcla4ev 1877	. . . . . . . . 9 |- (((z / 2) e. RR /\ (0 < (z / 2) /\ A.y e. X ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A))) -> E.x e. RR (0 < x /\ A.y e. X ((PCy) <_ x -> ((F` P)D(F` y)) <_ A)))
13		rehalfclt 6034	. . . . . . . . . 10 |- (z e. RR -> (z / 2) e. RR)
14	13	ad2antrl 406	. . . . . . . . 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 ((PCy) < z -> ((F` P)D(F` y)) < A)))) -> (z / 2) e. RR)
15	1	metcl 7811	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. Met /\ P e. X /\ y e. X) -> (PCy) e. RR)
16		halfpost 6036	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. RR -> (0 < z <-> (z / 2) < z))
17	16	biimpa 416	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. RR /\ 0 < z) -> (z / 2) < z)
18	17	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> (z / 2) < z)
19		lelttrt 5523	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ (z / 2) e. RR /\ z e. RR) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
20		pm3.26 319	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ z e. RR) -> (PCy) e. RR)
21	13	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ z e. RR) -> (z / 2) e. RR)
22		pm3.27 323	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((PCy) e. RR /\ z e. RR) -> z e. RR)
23	19, 20, 21, 22	syl3anc 858	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((PCy) e. RR /\ z e. RR) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
24	23	adantrr 395	. . . . . . . . . . . . . . . . . . . . . 22 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
25	18, 24	mpan2d 702	. . . . . . . . . . . . . . . . . . . . 21 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> ((PCy) <_ (z / 2) -> (PCy) < z))
26	25	ex 373	. . . . . . . . . . . . . . . . . . . 20 |- ((PCy) e. RR -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z)))
27	15, 26	syl 10	. . . . . . . . . . . . . . . . . . 19 |- ((C e. Met /\ P e. X /\ y e. X) -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z)))
28	27	3expia 835	. . . . . . . . . . . . . . . . . 18 |- ((C e. Met /\ P e. X) -> (y e. X -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z))))
29	28	com23 32	. . . . . . . . . . . . . . . . 17 |- ((C e. Met /\ P e. X) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
30	29	3adant2 798	. . . . . . . . . . . . . . . 16 |- ((C e. Met /\ D e. Met /\ P e. X) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
31	30	ad2antrr 404	. . . . . . . . . . . . . . 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 -> ((PCy) <_ (z / 2) -> (PCy) < z))))
32	31	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) -> ((PCy) <_ (z / 2) -> (PCy) < z))
33		ltlet 5520	. . . . . . . . . . . . . . . 16 |- ((((F` P)D(F` y)) e. RR /\ A e. RR) -> (((F` P)D(F` y)) < A -> ((F` P)D(F` y)) <_ A))
34	3	metcl 7811	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((D e. Met /\ (F` P) e. Y /\ (F` y) e. Y) -> ((F` P)D(F` y)) e. RR)
35	34	3expb 834	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((D e. Met /\ ((F` P) e. Y /\ (F` y) e. Y)) -> ((F` P)D(F` y)) e. RR)
36		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:X-->Y /\ P e. X) -> (F` P) e. Y)
37		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:X-->Y /\ y e. X) -> (F` y) e. Y)
38	36, 37	anim12i 333	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F:X-->Y /\ P e. X) /\ (F:X-->Y /\ y e. X)) -> ((F` P) e. Y /\ (F` y) e. Y))
39	38	anandis 512	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F:X-->Y /\ (P e. X /\ y e. X)) -> ((F` P) e. Y /\ (F` y) e. Y))
40	35, 39	sylan2 451	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D e. Met /\ (F:X-->Y /\ (P e. X /\ y e. X))) -> ((F` P)D(F` y)) e. RR)
41	40	exp45 386	. . . . . . . . . . . . . . . . . . . . 21 |- (D e. Met -> (F:X-->Y -> (P e. X -> (y e. X -> ((F` P)D(F` y)) e. RR))))
42	41	com23 32	. . . . . . . . . . . . . . . . . . . 20 |- (D e. Met -> (P e. X -> (F:X-->Y -> (y e. X -> ((F` P)D(F` y)) e. RR))))
43	42	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((D e. Met /\ P e. X) -> (F:X-->Y -> (y e. X -> ((F` P)D(F` y)) e. RR)))
44	43	3adant1 797	. . . . . . . . . . . . . . . . . 18 |- ((C e. Met /\ D e. Met /\ P e. X) -> (F:X-->Y -> (y e. X -> ((F` P)D(F` y)) e. RR)))
45	44	imp31 362	. . . . . . . . . . . . . . . . 17 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ y e. X) -> ((F` P)D(F` y)) e. RR)
46	45	adantlr 393	. . . . . . . . . . . . . . . 16 |- (((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (A e. RR