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 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑥𝑋𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑋 ( ( 𝑥 𝐶 𝑤 ) < 𝑧 → ( ( 𝐹𝑥 ) 𝐷 ( 𝐹𝑤 ) ) < 𝑦 ) ) ) )