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	$⊢ J = MetOpen (C)$
		metcnp4.4	$⊢ K = MetOpen (D)$
		metcnp4.5	$⊢ φ \to C \in ∞Met (X)$
		metcnp4.6	$⊢ φ \to D \in ∞Met (Y)$
		metcnp4.7	$⊢ φ \to P \in X$
	Assertion	metcnp4	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P))))$

Proof

Step	Hyp	Ref	Expression
1		metcnp4.3	$⊢ J = MetOpen (C)$
2		metcnp4.4	$⊢ K = MetOpen (D)$
3		metcnp4.5	$⊢ φ \to C \in ∞Met (X)$
4		metcnp4.6	$⊢ φ \to D \in ∞Met (Y)$
5		metcnp4.7	$⊢ φ \to P \in X$
6	1	met1stc	$⊢ C \in ∞Met (X) \to J \in 1^{st} 𝜔$
7	3 6	syl	$⊢ φ \to J \in 1^{st} 𝜔$
8	1	mopntopon	$⊢ C \in ∞Met (X) \to J \in TopOn (X)$
9	3 8	syl	$⊢ φ \to J \in TopOn (X)$
10	2	mopntopon	$⊢ D \in ∞Met (Y) \to K \in TopOn (Y)$
11	4 10	syl	$⊢ φ \to K \in TopOn (Y)$
12	7 9 11 5	1stccnp	$⊢ φ \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall f ((f : ℕ ⟶ X \land f \underset{t}{⇝} (J) P) \to (F \circ f) \underset{t}{⇝} (K) F (P))))$