Theorem metcni2 7834

Description: Epsilon-delta property of a continuous metric space function.

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
metcni2	|- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (P e. X /\ 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 metcni2

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	metcni 7833	. 2 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> E.z e. RR (0 < z /\ A.y e. X ((PCy) < z -> ((F` P)D(F` y)) < A)))
6		breq2 2613	. . . . . . 7 |- (x = (z / 2) -> (0 < x <-> 0 < (z / 2)))
7		breq2 2613	. . . . . . . . 9 |- (x = (z / 2) -> ((PCy) <_ x <-> (PCy) <_ (z / 2)))
8	7	imbi1d 611	. . . . . . . 8 |- (x = (z / 2) -> (((PCy) <_ x -> ((F` P)D(F` y)) <_ A) <-> ((PCy) <_ (z / 2) -> ((F` P)D(F` y)) <_ A)))
9	8	ralbidv 1655	. . . . . . 7 |- (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)))
10	6, 9	anbi12d 626	. . . . . 6 |- (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))))
11	10	rcla4ev 1868	. . . . 5 |- (((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)))
12		rehalfclt 5981	. . . . . 6 |- (z e. RR -> (z / 2) e. RR)
13	12	ad2antrl 406	. . . . 5 |- ((((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (P e. X /\ 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)
14	1	metcl 7750	. . . . . . . . . . . . . . . 16 |- ((C e. Met /\ P e. X /\ y e. X) -> (PCy) e. RR)
15		halfpost 5983	. . . . . . . . . . . . . . . . . . . 20 |- (z e. RR -> (0 < z <-> (z / 2) < z))
16	15	biimpa 416	. . . . . . . . . . . . . . . . . . 19 |- ((z e. RR /\ 0 < z) -> (z / 2) < z)
17	16	adantl 388	. . . . . . . . . . . . . . . . . 18 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> (z / 2) < z)
18		lelttrt 5496	. . . . . . . . . . . . . . . . . . . 20 |- (((PCy) e. RR /\ (z / 2) e. RR /\ z e. RR) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
19		pm3.26 319	. . . . . . . . . . . . . . . . . . . 20 |- (((PCy) e. RR /\ z e. RR) -> (PCy) e. RR)
20	12	adantl 388	. . . . . . . . . . . . . . . . . . . 20 |- (((PCy) e. RR /\ z e. RR) -> (z / 2) e. RR)
21		pm3.27 323	. . . . . . . . . . . . . . . . . . . 20 |- (((PCy) e. RR /\ z e. RR) -> z e. RR)
22	18, 19, 20, 21	syl3anc 856	. . . . . . . . . . . . . . . . . . 19 |- (((PCy) e. RR /\ z e. RR) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
23	22	adantrr 395	. . . . . . . . . . . . . . . . . 18 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> (((PCy) <_ (z / 2) /\ (z / 2) < z) -> (PCy) < z))
24	17, 23	mpan2d 700	. . . . . . . . . . . . . . . . 17 |- (((PCy) e. RR /\ (z e. RR /\ 0 < z)) -> ((PCy) <_ (z / 2) -> (PCy) < z))
25	24	ex 373	. . . . . . . . . . . . . . . 16 |- ((PCy) e. RR -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z)))
26	14, 25	syl 10	. . . . . . . . . . . . . . 15 |- ((C e. Met /\ P e. X /\ y e. X) -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z)))
27	26	3expia 833	. . . . . . . . . . . . . 14 |- ((C e. Met /\ P e. X) -> (y e. X -> ((z e. RR /\ 0 < z) -> ((PCy) <_ (z / 2) -> (PCy) < z))))
28	27	com23 32	. . . . . . . . . . . . 13 |- ((C e. Met /\ P e. X) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
29	28	3ad2antr1 810	. . . . . . . . . . . 12 |- ((C e. Met /\ (P e. X /\ A e. RR /\ 0 < A)) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
30	29	3ad2antl1 807	. . . . . . . . . . 11 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> ((z e. RR /\ 0 < z) -> (y e. X -> ((PCy) <_ (z / 2) -> (PCy) < z))))
31	30	imp31 362	. . . . . . . . . 10 |- (((((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) /\ (z e. RR /\ 0 < z)) /\ y e. X) -> ((PCy) <_ (z / 2) -> (PCy) < z))
32		ltlet 5493	. . . . . . . . . . . 12 |- ((((F` P)D(F` y)) e. RR /\ A e. RR) -> (((F` P)D(F` y)) < A -> ((F` P)D(F` y)) <_ A))
33	3	metcl 7750	. . . . . . . . . . . . . . . . . . . . 21 |- ((D e. Met /\ (F` P) e. Y /\ (F` y) e. Y) -> ((F` P)D(F` y)) e. RR)
34	33	3expb 832	. . . . . . . . . . . . . . . . . . . 20 |- ((D e. Met /\ ((F` P) e. Y /\ (F` y) e. Y)) -> ((F` P)D(F` y)) e. RR)
35		ffvelrn 3799	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:X-->Y /\ P e. X) -> (F` P) e. Y)
36		ffvelrn 3799	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F:X-->Y /\ y e. X) -> (F` y) e. Y)
37	35, 36	anim12i 333	. . . . . . . . . . . . . . . . . . . . 21 |- (((F:X-->Y /\ P e. X) /\ (F:X-->Y /\ y e. X)) -> ((F` P) e. Y /\ (F` y) e. Y))
38	37	anandis 511	. . . . . . . . . . . . . . . . . . . 20 |- ((F:X-->Y /\ (P e. X /\ y e. X)) -> ((F` P) e. Y /\ (F` y) e. Y))
39	34, 38	sylan2 451	. . . . . . . . . . . . . . . . . . 19 |- ((D e. Met /\ (F:X-->Y /\ (P e. X /\ y e. X))) -> ((F` P)D(F` y)) e. RR)
40	39	exp45 386	. . . . . . . . . . . . . . . . . 18 |- (D e. Met -> (F:X-->Y -> (P e. X -> (y e. X -> ((F` P)D(F` y)) e. RR))))
41	40	imp 350	. . . . . . . . . . . . . . . . 17 |- ((D e. Met /\ F:X-->Y) -> (P e. X -> (y e. X -> ((F` P)D(F` y)) e. RR)))
42	41	3adant1 795	. . . . . . . . . . . . . . . 16 |- ((C e. Met /\ D e. Met /\ F:X-->Y) -> (P e. X -> (y e. X -> ((F` P)D(F` y)) e. RR)))
43	1, 3, 2, 4	metcnf 7823	. . . . . . . . . . . . . . . 16 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> F:X-->Y)
44	42, 43	syl3dan3 868	. . . . . . . . . . . . . . 15 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> (P e. X -> (y e. X -> ((F` P)D(F` y)) e. RR)))
45	44	imp 350	. . . . . . . . . . . . . 14 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ P e. X) -> (y e. X -> ((F` P)D(F` y)) e. RR))
46	45	3ad2antr1 810	. . . . . . . . . . . . 13 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (P e. X /\ A e. RR /\ 0 < A)) -> (y e. X -> ((F` P)D(F