Theorem metcn 7898

Description: Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D.

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
metcn	|- ((C e. Met /\ D e. Met) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.x e. X A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))

Distinct variable groups:   x,w,y,z,F   w,C,x,y,z   w,D,x,y,z   w,X,x,y,z   w,Y,x,y,z   w,J,x,y,z   x,K,y

Proof of Theorem metcn

Step	Hyp	Ref	Expression
1		eqid 1482	. . . . . . 7 |- U.J = U.J
2		eqid 1482	. . . . . . 7 |- U.K = U.K
3	1, 2	cnf 7771	. . . . . 6 |- ((J e. Top /\ K e. Top /\ F e. (J Cn K)) -> F:U.J-->U.K)
4	3	3expia 839	. . . . 5 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) -> F:U.J-->U.K))
5	4	pm4.71rd 642	. . . 4 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:U.J-->U.K /\ F e. (J Cn K))))
6	1, 2	cncnp 7787	. . . . . 6 |- ((J e. Top /\ K e. Top /\ F:U.J-->U.K) -> (F e. (J Cn K) <-> A.x e. U.JF e. ((J CnP K)` x)))
7	6	3expa 837	. . . . 5 |- (((J e. Top /\ K e. Top) /\ F:U.J-->U.K) -> (F e. (J Cn K) <-> A.x e. U.JF e. ((J CnP K)` x)))
8	7	pm5.32da 652	. . . 4 |- ((J e. Top /\ K e. Top) -> ((F:U.J-->U.K /\ F e. (J Cn K)) <-> (F:U.J-->U.K /\ A.x e. U.JF e. ((J CnP K)` x))))
9	5, 8	bitrd 531	. . 3 |- ((J e. Top /\ K e. Top) -> (F e. (J Cn K) <-> (F:U.J-->U.K /\ A.x e. U.JF e. ((J CnP K)` x))))
10		metcn.2	. . . 4 |- J = (Open` C)
11	10	opntop 7879	. . 3 |- (C e. Met -> J e. Top)
12		metcn.4	. . . 4 |- K = (Open` D)
13	12	opntop 7879	. . 3 |- (D e. Met -> K e. Top)
14	9, 11, 13	syl2an 457	. 2 |- ((C e. Met /\ D e. Met) -> (F e. (J Cn K) <-> (F:U.J-->U.K /\ A.x e. U.JF e. ((J CnP K)` x))))
15		feq23 3637	. . . . . . . . . . 11 |- ((U.J = X /\ U.K = Y) -> (F:U.J-->U.K <-> F:X-->Y))
16		metcn.1	. . . . . . . . . . . 12 |- X = dom dom C
17	16, 10	uniopn 7870	. . . . . . . . . . 11 |- (C e. Met -> U.J = X)
18		metcn.3	. . . . . . . . . . . 12 |- Y = dom dom D
19	18, 12	uniopn 7870	. . . . . . . . . . 11 |- (D e. Met -> U.K = Y)
20	15, 17, 19	syl2an 457	. . . . . . . . . 10 |- ((C e. Met /\ D e. Met) -> (F:U.J-->U.K <-> F:X-->Y))
21	20	adantr 391	. . . . . . . . 9 |- (((C e. Met /\ D e. Met) /\ x e. U.J) -> (F:U.J-->U.K <-> F:X-->Y))
22	21	anbi1d 620	. . . . . . . 8 |- (((C e. Met /\ D e. Met) /\ x e. U.J) -> ((F:U.J-->U.K /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y)))) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))
23	17	adantr 391	. . . . . . . . . . 11 |- ((C e. Met /\ D e. Met) -> U.J = X)
24	23	eleq2d 1548	. . . . . . . . . 10 |- ((C e. Met /\ D e. Met) -> (x e. U.J <-> x e. X))
25	24	biimpa 418	. . . . . . . . 9 |- (((C e. Met /\ D e. Met) /\ x e. U.J) -> x e. X)
26	16, 10, 18, 12	metcnp 7896	. . . . . . . . . 10 |- ((C e. Met /\ D e. Met /\ x e. X) -> (F e. ((J CnP K)` x) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))
27	26	3expa 837	. . . . . . . . 9 |- (((C e. Met /\ D e. Met) /\ x e. X) -> (F e. ((J CnP K)` x) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))
28	25, 27	syldan 470	. . . . . . . 8 |- (((C e. Met /\ D e. Met) /\ x e. U.J) -> (F e. ((J CnP K)` x) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))
29	1, 2	cnpf 7772	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ x e. U.J) /\ F e. ((J CnP K)` x)) -> F:U.J-->U.K)
30	29	ex 373	. . . . . . . . . . . 12 |- ((J e. Top /\ K e. Top /\ x e. U.J) -> (F e. ((J CnP K)` x) -> F:U.J-->U.K))
31	30	pm4.71rd 642	. . . . . . . . . . 11 |- ((J e. Top /\ K e. Top /\ x e. U.J) -> (F e. ((J CnP K)` x) <-> (F:U.J-->U.K /\ F e. ((J CnP K)` x))))
32	31	3expia 839	. . . . . . . . . 10 |- ((J e. Top /\ K e. Top) -> (x e. U.J -> (F e. ((J CnP K)` x) <-> (F:U.J-->U.K /\ F e. ((J CnP K)` x)))))
33	32, 11, 13	syl2an 457	. . . . . . . . 9 |- ((C e. Met /\ D e. Met) -> (x e. U.J -> (F e. ((J CnP K)` x) <-> (F:U.J-->U.K /\ F e. ((J CnP K)` x)))))
34	33	imp 350	. . . . . . . 8 |- (((C e. Met /\ D e. Met) /\ x e. U.J) -> (F e. ((J CnP K)` x) <-> (F:U.J-->U.K /\ F e. ((J CnP K)` x))))
35	22, 28, 34	3bitr2rd 550	. . . . . . 7 |- (((C e. Met /\ D e. Met) /\ x e. U.J) -> ((F:U.J-->U.K /\ F e. ((J CnP K)` x)) <-> (F:U.J-->U.K /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))
36		pm5.32 647	. . . . . . 7 |- ((F:U.J-->U.K -> (F e. ((J CnP K)` x) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))) <-> ((F:U.J-->U.K /\ F e. ((J CnP K)` x)) <-> (F:U.J-->U.K /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))
37	35, 36	sylibr 200	. . . . . 6 |- (((C e. Met /\ D e. Met) /\ x e. U.J) -> (F:U.J-->U.K -> (F e. ((J CnP K)` x) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))
38	37	imp 350	. . . . 5 |- ((((C e. Met /\ D e. Met) /\ x e. U.J) /\ F:U.J-->U.K) -> (F e. ((J CnP K)` x) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y)))))
39	38	an1rs 492	. . . 4 |- ((((C e. Met /\ D e. Met) /\ F:U.J-->U.K) /\ x e. U.J) -> (F e. ((J CnP K)` x) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y)))))
40	39	ralbidva 1666	. . 3 |- (((C e. Met /\ D e. Met) /\ F:U.J-->U.K) -> (A.x e. U.JF e. ((J CnP K)` x) <-> A.x e. U.JA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y)))))
41	40	pm5.32da 652	. 2 |- ((C e. Met /\ D e. Met) -> ((F:U.J-->U.K /\ A.x e. U.JF e. ((J CnP K)` x)) <-> (F:U.J-->U.K /\ A.x e. U.JA.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> (