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	$$⊢J=\mathrm{MetOpen}\left(C\right)$$
	metcnp4.4	$$⊢K=\mathrm{MetOpen}\left(D\right)$$
	metcnp4.5	$$⊢\phi \to C\in \mathrm{\infty Met}\left(X\right)$$
	metcnp4.6	$$⊢\phi \to D\in \mathrm{\infty Met}\left(Y\right)$$
	metcn4.7	$$⊢\phi \to F:X⟶Y$$
Assertion	metcn4	$$⊢\phi \to \left(F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \forall f\left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		metcnp4.3	$$⊢J=\mathrm{MetOpen}\left(C\right)$$
2		metcnp4.4	$$⊢K=\mathrm{MetOpen}\left(D\right)$$
3		metcnp4.5	$$⊢\phi \to C\in \mathrm{\infty Met}\left(X\right)$$
4		metcnp4.6	$$⊢\phi \to D\in \mathrm{\infty Met}\left(Y\right)$$
5		metcn4.7	$$⊢\phi \to F:X⟶Y$$
6	1	met1stc	$$⊢C\in \mathrm{\infty Met}\left(X\right)\to J\in 1^{st}𝜔$$
7	3 6	syl	$$⊢\phi \to J\in 1^{st}𝜔$$
8	1	mopntopon	$$⊢C\in \mathrm{\infty Met}\left(X\right)\to J\in \mathrm{TopOn}\left(X\right)$$
9	3 8	syl	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
10	2	mopntopon	$$⊢D\in \mathrm{\infty Met}\left(Y\right)\to K\in \mathrm{TopOn}\left(Y\right)$$
11	4 10	syl	$$⊢\phi \to K\in \mathrm{TopOn}\left(Y\right)$$
12	7 9 11 5	1stccn	$$⊢\phi \to \left(F\in \left(J\mathrm{Cn}K\right)\leftrightarrow \forall f\left(f:\mathbb{N}⟶X\to \forall x\left(f\underset{t}{⇝}\left(J\right)x\to \left(F\circ f\right)\underset{t}{⇝}\left(K\right)F\left(x\right)\right)\right)\right)$$