Theorem metcnp4 7904

Description: Two ways to say a mapping from metric C to metric D is continuous at point P. Theorem 14-4.3 of [Gleason] p. 240.

Hypotheses

Ref	Expression
metcnp4.1	|- X = dom dom C
metcnp4.3	|- Y = dom dom D
metcnp4.c	|- J = (Open` C)
metcnp4.d	|- K = (Open` D)
metcnp4.5	|- G = {<.j, y>. | (j e. NN /\ y = (F` (f` j)))}

Assertion

Ref	Expression
metcnp4	|- ((C e. Met /\ D e. Met /\ P e. X) -> (F e. ((J CnP K)` P) <-> (F:X-->Y /\ A.f((f:NN-->X /\ f(~~>m` C)P) -> G(~~>m` D)(F` P)))))

Distinct variable groups:   C,f   D,f   f,j,y,F   P,f   f,X,j   f,Y,j,y

Proof of Theorem metcnp4

Step	Hyp	Ref	Expression
1		metcnp4.1	. . 3 |- X = dom dom C
2		metcnp4.c	. . 3 |- J = (Open` C)
3		metcnp4.3	. . 3 |- Y = dom dom D
4		metcnp4.d	. . 3 |- K = (Open` D)
5	1, 2, 3, 4	metcnp2 7827	. 2 |- ((C e. Met /\ D e. Met /\ P e. X) -> (F e. ((J CnP K)` P) <-> (F:X-->Y /\ A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))))))
6		metcnp4.5	. . . . . . . . . . 11 |- G = {<.j, y>. | (j e. NN /\ y = (F` (f` j)))}
7	1, 3, 2, 4, 6	metcnp4lem2 7903	. . . . . . . . . 10 |- (((C e. Met /\ P e. X) /\ F:X-->Y) -> ((f:NN-->X /\ f(~~>m` C)P) -> (A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))) -> A.x e. RR (0 < x -> E.k e. NN A.m e. NN (k <_ m -> ((G` m)D(F` P)) < x)))))
8	7	3adantl2 802	. . . . . . . . 9 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) -> ((f:NN-->X /\ f(~~>m` C)P) -> (A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))) -> A.x e. RR (0 < x -> E.k e. NN A.m e. NN (k <_ m -> ((G` m)D(F` P)) < x)))))
9	8	imp 350	. . . . . . . 8 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (f:NN-->X /\ f(~~>m` C)P)) -> (A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))) -> A.x e. RR (0 < x -> E.k e. NN A.m e. NN (k <_ m -> ((G` m)D(F` P)) < x))))
10		1z 6106	. . . . . . . . . . 11 |- 1 e. ZZ
11		nnuz 6371	. . . . . . . . . . 11 |- NN = (ZZ>` 1)
12	3, 10, 11	lmbrf2 7869	. . . . . . . . . 10 |- ((D e. Met /\ (F` P) e. Y /\ G:NN-->Y) -> (G(~~>m` D)(F` P) <-> A.x e. RR (0 < x -> E.k e. NN A.m e. NN (k <_ m -> ((G` m)D(F` P)) < x))))
13		3simp2 787	. . . . . . . . . . 11 |- ((C e. Met /\ D e. Met /\ P e. X) -> D e. Met)
14	13	ad2antrr 404	. . . . . . . . . 10 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ f:NN-->X) -> D e. Met)
15		ffvelrn 3799	. . . . . . . . . . . . 13 |- ((F:X-->Y /\ P e. X) -> (F` P) e. Y)
16	15	ancoms 436	. . . . . . . . . . . 12 |- ((P e. X /\ F:X-->Y) -> (F` P) e. Y)
17	16	3ad2antl3 809	. . . . . . . . . . 11 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) -> (F` P) e. Y)
18	17	adantr 389	. . . . . . . . . 10 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ f:NN-->X) -> (F` P) e. Y)
19		ffvelrn 3799	. . . . . . . . . . . . . . 15 |- ((F:X-->Y /\ (f` j) e. X) -> (F` (f` j)) e. Y)
20		ffvelrn 3799	. . . . . . . . . . . . . . 15 |- ((f:NN-->X /\ j e. NN) -> (f` j) e. X)
21	19, 20	sylan2 451	. . . . . . . . . . . . . 14 |- ((F:X-->Y /\ (f:NN-->X /\ j e. NN)) -> (F` (f` j)) e. Y)
22	21	anassrs 441	. . . . . . . . . . . . 13 |- (((F:X-->Y /\ f:NN-->X) /\ j e. NN) -> (F` (f` j)) e. Y)
23	22	r19.21aiva 1706	. . . . . . . . . . . 12 |- ((F:X-->Y /\ f:NN-->X) -> A.j e. NN (F` (f` j)) e. Y)
24	6	fopab2 3808	. . . . . . . . . . . 12 |- (A.j e. NN (F` (f` j)) e. Y <-> G:NN-->Y)
25	23, 24	sylib 198	. . . . . . . . . . 11 |- ((F:X-->Y /\ f:NN-->X) -> G:NN-->Y)
26	25	adantll 392	. . . . . . . . . 10 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ f:NN-->X) -> G:NN-->Y)
27	12, 14, 18, 26	syl3anc 856	. . . . . . . . 9 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ f:NN-->X) -> (G(~~>m` D)(F` P) <-> A.x e. RR (0 < x -> E.k e. NN A.m e. NN (k <_ m -> ((G` m)D(F` P)) < x))))
28	27	adantrr 395	. . . . . . . 8 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (f:NN-->X /\ f(~~>m` C)P)) -> (G(~~>m` D)(F` P) <-> A.x e. RR (0 < x -> E.k e. NN A.m e. NN (k <_ m -> ((G` m)D(F` P)) < x))))
29	9, 28	sylibrd 204	. . . . . . 7 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (f:NN-->X /\ f(~~>m` C)P)) -> (A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))) -> G(~~>m` D)(F` P)))
30	29	ex 373	. . . . . 6 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) -> ((f:NN-->X /\ f(~~>m` C)P) -> (A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))) -> G(~~>m` D)(F` P))))
31	30	com23 32	. . . . 5 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) -> (A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))) -> ((f:NN-->X /\ f(~~>m` C)P) -> G(~~>m` D)(F` P))))
32	31	19.21adv 1283	. . . 4 |- (((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) -> (A.x e. RR (0 < x -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < x))) -> A.f((f:NN-->X /\ f(~~>m` C)P) -> G(~~>m` D)(F` P))))
33		simprl 414	. . . . . . . . . . . . . . 15 |- (((C e. Met /\ P e. X) /\ (f:NN-->X /\ A.k e. NN ((f` k)CP) < (1 / k))) -> f:NN-->X)
34	1	lmnn 7873	. . . . . . . . . . . . . . 15 |- (((C e. Met /\ P e. X) /\ (f:NN-->X /\ A.k e. NN ((f` k)CP) < (1 / k))) -> f(~~>m` C)P)
35	33, 34	jca 288	. . . . . . . . . . . . . 14 |- (((C e. Met /\ P e. X) /\ (f:NN-->X /\ A.k e. NN ((f` k)CP) < (1 / k))) -> (f:NN-->X /\ f(~~>m` C)P))
36	35	ex 373	. . . . . . . . . . . . 13 |- ((C e. Met /\ P e. X) -> ((f:NN-->X /\ A.k e. NN ((f` k)CP) < (1 / k)) -> (f:NN-->X /\ f(~~>m` C)P)))
37	36	3adant2 796	. . . . . . . . . . . 12 |- ((C e. Met /\ D e. Met /\ P e. X) -> ((f:NN-->X /\ A.k e. NN ((f` k)CP) < (1 / k)) -> (f:NN-->X /\ f(~~>m` C)P)))
38	37	ad2antrr 404	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met /\ P e. X) /\ F:X-->Y) /\ (x e. RR /\ 0 < x)) -> ((f:NN-->X /\ A.k e. NN ((f` k)CP) < (1 / k)) -> (f