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 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑋 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑃 ) ) ) ) )