Theorem metcn4

Description: Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.3 of Munkres p. 128. (Contributed by NM, 13-Jun-2007) (Revised by Mario Carneiro, 4-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		metcnp4.3	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2		metcnp4.4	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3		metcnp4.5	⊢ ( 𝜑 → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
4		metcnp4.6	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
5		metcn4.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	1stccn	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑓 ( 𝑓 : ℕ ⟶ 𝑋 → ∀ 𝑥 ( 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 → ( 𝐹 ∘ 𝑓 ) ( ⇝𝑡 ‘ 𝐾 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )