cnpf2

Description: A continuous function at point P is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	cnpf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2		eqid	$⊢ ⋃ K = ⋃ K$
3	1 2	cnpf	$⊢ F \in (J CnP K) (P) \to F : ⋃ J ⟶ ⋃ K$
4		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
5	4	feq2d	$⊢ J \in TopOn (X) \to (F : X ⟶ Y \leftrightarrow F : ⋃ J ⟶ Y)$
6		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
7	6	feq3d	$⊢ K \in TopOn (Y) \to (F : ⋃ J ⟶ Y \leftrightarrow F : ⋃ J ⟶ ⋃ K)$
8	5 7	sylan9bb	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F : X ⟶ Y \leftrightarrow F : ⋃ J ⟶ ⋃ K)$
9	3 8	imbitrrid	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J CnP K) (P) \to F : X ⟶ Y)$
10	9	3impia	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$

Metamath Proof Explorer