HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem metcnp3 7879
Description: Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of [Gleason] p. 240.
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
metcnp3 |- ((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 /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y))))))
Distinct variable groups:   y,z,F   y,C,z   y,D,z   y,X,z   y,Y,z   y,P,z   y,J,z   y,K
Proof of Theorem metcnp3
StepHypRef 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)
51, 2, 3, 4metcnp 7870 . 2 |- ((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))))))
6 funimass3 3803 . . . . . . . . . . . . . 14 |- ((Fun F /\ (P( ball ` C)z) (_ dom F) -> ((F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y) <-> (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y))))
7 ffun 3626 . . . . . . . . . . . . . . . 16 |- (F:X-->Y -> Fun F)
87adantr 389 . . . . . . . . . . . . . . 15 |- ((F:X-->Y /\ P e. X) -> Fun F)
98ad2antlr 405 . . . . . . . . . . . . . 14 |- (((C e. Met /\ (F:X-->Y /\ P e. X)) /\ (z e. RR /\ 0 < z)) -> Fun F)
101blssm 7832 . . . . . . . . . . . . . . . 16 |- (((C e. Met /\ P e. X) /\ (z e. RR /\ 0 < z)) -> (P( ball ` C)z) (_ X)
1110adantlrl 398 . . . . . . . . . . . . . . 15 |- (((C e. Met /\ (F:X-->Y /\ P e. X)) /\ (z e. RR /\ 0 < z)) -> (P( ball ` C)z) (_ X)
12 fdm 3628 . . . . . . . . . . . . . . . . 17 |- (F:X-->Y -> dom F = X)
1312adantr 389 . . . . . . . . . . . . . . . 16 |- ((F:X-->Y /\ P e. X) -> dom F = X)
1413ad2antlr 405 . . . . . . . . . . . . . . 15 |- (((C e. Met /\ (F:X-->Y /\ P e. X)) /\ (z e. RR /\ 0 < z)) -> dom F = X)
1511, 14sseqtr4d 2096 . . . . . . . . . . . . . 14 |- (((C e. Met /\ (F:X-->Y /\ P e. X)) /\ (z e. RR /\ 0 < z)) -> (P( ball ` C)z) (_ dom F)
166, 9, 15sylanc 471 . . . . . . . . . . . . 13 |- (((C e. Met /\ (F:X-->Y /\ P e. X)) /\ (z e. RR /\ 0 < z)) -> ((F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y) <-> (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y))))
1716anassrs 441 . . . . . . . . . . . 12 |- ((((C e. Met /\ (F:X-->Y /\ P e. X)) /\ z e. RR) /\ 0 < z) -> ((F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y) <-> (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y))))
1817pm5.32da 648 . . . . . . . . . . 11 |- (((C e. Met /\ (F:X-->Y /\ P e. X)) /\ z e. RR) -> ((0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y)) <-> (0 < z /\ (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y)))))
1918rexbidva 1659 . . . . . . . . . 10 |- ((C e. Met /\ (F:X-->Y /\ P e. X)) -> (E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y)) <-> E.z e. RR (0 < z /\ (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y)))))
2019imbi2d 611 . . . . . . . . 9 |- ((C e. Met /\ (F:X-->Y /\ P e. X)) -> ((0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y))) <-> (0 < y -> E.z e. RR (0 < z /\ (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y))))))
2120ralbidv 1662 . . . . . . . 8 |- ((C e. Met /\ (F:X-->Y /\ P e. X)) -> (A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y))) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y))))))
2221adantlr 393 . . . . . . 7 |- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> (A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y))) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y))))))
231, 2, 3, 4metcnplem 7869 . . . . . . 7 |- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> (A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)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)))))
2422, 23bitr2d 528 . . . . . 6 |- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> (A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((PCw) < z -> ((F` P)D(F` w)) < y))) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y)))))
2524anassrs 441 . . . . 5 |- ((((C e. Met /\ D e. Met) /\ F:X-->Y) /\ P e. X) -> (A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((PCw) < z -> ((F` P)D(F` w)) < y))) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y)))))
2625an1rs 489 . . . 4 |- ((((C e. Met /\ D e. Met) /\ P e. X) /\ 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))) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y)))))
2726pm5.32da 648 . . 3 |- (((C e. Met /\ D e. Met) /\ P e. X) -> ((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)))) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y))))))
28273impa 827 . 2 |- ((C e. Met /\ D e. Met /\ P e. X) -> ((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)))) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y))))))
295, 28bitrd 527 1 |- ((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 /\ (F"(P( ball ` C)z)) (_ ((F` P)( ball ` D)y))))))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 774   = wceq 955   e. wcel 957  A.wral 1644  E.wrex 1645   (_ wss 2045   class class class wbr 2616  `'ccnv 3166  dom cdm 3167  "cima 3170  Fun wfun 3173  --><