Metamath Proof Explorer

Theorem metcn

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 . (Contributed by NM, 15-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses metcn.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
metcn.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
Assertion metcn ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 metcn.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
2 metcn.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
3 1 mopntopon ⊒ ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
4 2 mopntopon ⊒ ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) β†’ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) )
5 cncnp ⊒ ( ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) ∧ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ π‘₯ ) ) ) )
6 3 4 5 syl2an ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ π‘₯ ) ) ) )
7 simplr ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
8 1 2 metcnp ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ π‘₯ ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
9 8 ad4ant124 ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ π‘₯ ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
10 7 9 mpbirand ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ π‘₯ ) ↔ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
11 10 ralbidva ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ π‘₯ ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ π‘₯ ) ↔ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
12 11 pm5.32da ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ π‘₯ ) ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
13 6 12 bitrd ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ) β†’ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( π‘₯ 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ π‘₯ ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )