This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metcnp4

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . Theorem 14-4.3 of Gleason p. 240. (Contributed by NM, 17-May-2007) (Revised by Mario Carneiro, 4-May-2014)

Ref Expression
Hypotheses metcnp4.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metcnp4.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
metcnp4.5 ⊢ ( 𝜑 → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
metcnp4.6 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
metcnp4.7 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
Assertion metcnp4 ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 metcnp4.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metcnp4.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 metcnp4.5 ⊢ ( 𝜑 → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
4 metcnp4.6 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
5 metcnp4.7 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
6 1 met1stc ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ 1stω )
7 3 6 syl ⊢ ( 𝜑 → 𝐽 ∈ 1stω )
8 1 mopntopon ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9 3 8 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 2 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
11 4 10 syl ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
12 7 9 11 5 1stccnp ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) )