Theorem metcnp 7887

Description: Two ways to say a mapping from metric C to metric D is continuous at point P. Warning: The HTML proof page is 0.6 megabyte in size.

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
metcnp	|- ((C e. Met /\ D e. Met /\ P e. X) -> (F e. ((J CnP K)` P) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((PCw) < z -> ((F` P)D(F` w)) < y))))))

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

Proof of Theorem metcnp

Step	Hyp	Ref	Expression
1		eqid 1475	. . . 4 |- U.J = U.J
2		eqid 1475	. . . 4 |- U.K = U.K
3	1, 2	iscnp 7760	. . 3 |- ((J e. Top /\ K e. Top /\ P e. U.J) -> (F e. ((J CnP K)` P) <-> (F:U.J-->U.K /\ A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)))))
4		metcn.2	. . . . 5 |- J = (Open` C)
5	4	opntop 7870	. . . 4 |- (C e. Met -> J e. Top)
6	5	3ad2ant1 800	. . 3 |- ((C e. Met /\ D e. Met /\ P e. X) -> J e. Top)
7		metcn.4	. . . . 5 |- K = (Open` D)
8	7	opntop 7870	. . . 4 |- (D e. Met -> K e. Top)
9	8	3ad2ant2 801	. . 3 |- ((C e. Met /\ D e. Met /\ P e. X) -> K e. Top)
10		metcn.1	. . . . . . 7 |- X = dom dom C
11	10, 4	uniopn 7861	. . . . . 6 |- (C e. Met -> U.J = X)
12	11	eleq2d 1541	. . . . 5 |- (C e. Met -> (P e. U.J <-> P e. X))
13	12	biimpar 417	. . . 4 |- ((C e. Met /\ P e. X) -> P e. U.J)
14	13	3adant2 798	. . 3 |- ((C e. Met /\ D e. Met /\ P e. X) -> P e. U.J)
15	3, 6, 9, 14	syl3anc 858	. 2 |- ((C e. Met /\ D e. Met /\ P e. X) -> (F e. ((J CnP K)` P) <-> (F:U.J-->U.K /\ A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)))))
16		feq23 3623	. . . . 5 |- ((U.J = X /\ U.K = Y) -> (F:U.J-->U.K <-> F:X-->Y))
17		metcn.3	. . . . . 6 |- Y = dom dom D
18	17, 7	uniopn 7861	. . . . 5 |- (D e. Met -> U.K = Y)
19	16, 11, 18	syl2an 454	. . . 4 |- ((C e. Met /\ D e. Met) -> (F:U.J-->U.K <-> F:X-->Y))
20	19	anbi1d 617	. . 3 |- ((C e. Met /\ D e. Met) -> ((F:U.J-->U.K /\ A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v))) <-> (F:X-->Y /\ A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)))))
21	20	3adant3 799	. 2 |- ((C e. Met /\ D e. Met /\ P e. X) -> ((F:U.J-->U.K /\ A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v))) <-> (F:X-->Y /\ A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)))))
22		eleq2 1535	. . . . . . . . . . . . . . . . . . 19 |- (v = ((F` P)( ball ` D)y) -> ((F` P) e. v <-> (F` P) e. ((F` P)( ball ` D)y)))
23		sseq2 2083	. . . . . . . . . . . . . . . . . . . . 21 |- (v = ((F` P)( ball ` D)y) -> ((F"u) (_ v <-> (F"u) (_ ((F` P)( ball ` D)y)))
24	23	anbi2d 616	. . . . . . . . . . . . . . . . . . . 20 |- (v = ((F` P)( ball ` D)y) -> ((P e. u /\ (F"u) (_ v) <-> (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y))))
25	24	rexbidv 1664	. . . . . . . . . . . . . . . . . . 19 |- (v = ((F` P)( ball ` D)y) -> (E.u e. J (P e. u /\ (F"u) (_ v) <-> E.u e. J (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y))))
26	22, 25	imbi12d 626	. . . . . . . . . . . . . . . . . 18 |- (v = ((F` P)( ball ` D)y) -> (((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)) <-> ((F` P) e. ((F` P)( ball ` D)y) -> E.u e. J (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y)))))
27	26	rcla4v 1873	. . . . . . . . . . . . . . . . 17 |- (((F` P)( ball ` D)y) e. K -> (A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)) -> ((F` P) e. ((F` P)( ball ` D)y) -> E.u e. J (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y)))))
28	27	com23 32	. . . . . . . . . . . . . . . 16 |- (((F` P)( ball ` D)y) e. K -> ((F` P) e. ((F` P)( ball ` D)y) -> (A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)) -> E.u e. J (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y)))))
29	17, 7	blopn 7876	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ (F` P) e. Y) /\ (y e. RR /\ 0 < y)) -> ((F` P)( ball ` D)y) e. K)
30	17	blcntr 7845	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ (F` P) e. Y) /\ (y e. RR /\ 0 < y)) -> (F` P) e. ((F` P)( ball ` D)y))
31	28, 29, 30	sylc 68	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ (F` P) e. Y) /\ (y e. RR /\ 0 < y)) -> (A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)) -> E.u e. J (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y))))
32		ffvelrn 3814	. . . . . . . . . . . . . . 15 |- ((F:X-->Y /\ P e. X) -> (F` P) e. Y)
33	31, 32	sylanl2 461	. . . . . . . . . . . . . 14 |- (((D e. Met /\ (F:X-->Y /\ P e. X)) /\ (y e. RR /\ 0 < y)) -> (A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)) -> E.u e. J (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y))))
34	33	adantlll 396	. . . . . . . . . . . . 13 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ (y e. RR /\ 0 < y)) -> (A.v e. K ((F` P) e. v -> E.u e. J (P e. u /\ (F"u) (_ v)) -> E.u e. J (P e. u /\ (F"u) (_ ((F` P)( ball ` D)y))))
35		funimass3 3806	. . . . . . . . . . . . . . . . . . . . 21 |- ((Fun F /\ u (_ dom F) -> ((F"u) (_ ((F` P)( ball ` D)y) <-> u (_ (`'F"((F` P)( ball ` D)y))))
36		ffun 3629	. . . . . . . . . . . . . . . . . . . . . 22 |- (F:X-->Y -> Fun F)
37	36	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . 21 |- (((C e. Met /\ F:X-->Y) /\ u e. J) -> Fun F)
38	10, 4	opnss 7863	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((C e. Met /\ u e. J) -> u (_ X)
39	38	adantlr 393	. . . . . . . . . . . . . . . . . . . . . 22 |- (((C e. Met /\ F:X-->Y) /\ u e. J) -> u (_ X)
40		fdm 3631	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F:X-->Y -> dom F = X)
41	40	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . 22 |- (((C e. Met /\ F:X-->Y) /\ u e. J) -> dom F = X)
42	39, 41	sseqtr4d 2098	. . . . . . . . . . . . . . . . . . . . 21 |- (((C e. Met /\ F:X-->Y) /\ u e. J) -> u (_ dom F)
43	35, 37, 42	sylanc 471	. . . . . . . . . . . . . . . . . . . 20 |- (((C e. Met /\ F:X-->Y) /\ u e. J) -> ((F"u) (_ ((F` P)( ball ` D)y) <-> u (_ (`'F"((F` P)( ball ` D)y))))
44	43	adantr 389	. . . . . . . . . . . . . . . . . . 19 |- ((((C e. Met /\ F:X-->Y) /\ u e. J) /\ P e. u) -> ((F"u) (_ ((F` P)( ball ` D)y) <-> u (_ (`'F"((F` P)( ball ` D)y))))
45		sstr 2072	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((P( ball ` C)z) (_ u /\ u (_ (`'F"((F` P)( ball ` D)y))) -> (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y)))
46	45	expcom 374	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u (_ (`'F"((F` P)( ball ` D)y)) -> ((P( ball ` C)z) (_ u -> (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y))))
47	46	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((u (_ (`'F"(