cnpdis

Description: If A is an isolated point in X (or equivalently, the singleton { A } is open in X ), then every function is continuous at A . (Contributed by Mario Carneiro, 9-Sep-2015)

		Ref	Expression
	Assertion	cnpdis	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to (J CnP K) (A) = Y^{X}$

Proof

Step	Hyp	Ref	Expression
1		simplrl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to \{A\} \in J$
2		simpll3	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to A \in X$
3		snidg	$⊢ A \in X \to A \in \{A\}$
4	2 3	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to A \in \{A\}$
5		simprr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to f (A) \in x$
6		simplrr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to f : X ⟶ Y$
7		ffn	$⊢ f : X ⟶ Y \to f Fn X$
8		elpreima	$⊢ f Fn X \to (A \in f^{-1} [x] \leftrightarrow (A \in X \land f (A) \in x))$
9	6 7 8	3syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to (A \in f^{-1} [x] \leftrightarrow (A \in X \land f (A) \in x))$
10	2 5 9	mpbir2and	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to A \in f^{-1} [x]$
11	10	snssd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to \{A\} \subseteq f^{-1} [x]$
12		eleq2	$⊢ y = \{A\} \to (A \in y \leftrightarrow A \in \{A\})$
13		sseq1	$⊢ y = \{A\} \to (y \subseteq f^{-1} [x] \leftrightarrow \{A\} \subseteq f^{-1} [x])$
14	12 13	anbi12d	$⊢ y = \{A\} \to ((A \in y \land y \subseteq f^{-1} [x]) \leftrightarrow (A \in \{A\} \land \{A\} \subseteq f^{-1} [x]))$
15	14	rspcev	$⊢ (\{A\} \in J \land (A \in \{A\} \land \{A\} \subseteq f^{-1} [x])) \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x])$
16	1 4 11 15	syl12anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land (x \in K \land f (A) \in x)) \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x])$
17	16	expr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \land x \in K) \to (f (A) \in x \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x]))$
18	17	ralrimiva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land (\{A\} \in J \land f : X ⟶ Y)) \to \forall x \in K (f (A) \in x \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x]))$
19	18	expr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to (f : X ⟶ Y \to \forall x \in K (f (A) \in x \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x])))$
20	19	pm4.71d	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to (f : X ⟶ Y \leftrightarrow (f : X ⟶ Y \land \forall x \in K (f (A) \in x \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x]))))$
21		simpl2	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to K \in TopOn (Y)$
22		toponmax	$⊢ K \in TopOn (Y) \to Y \in K$
23	21 22	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to Y \in K$
24		simpl1	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to J \in TopOn (X)$
25		toponmax	$⊢ J \in TopOn (X) \to X \in J$
26	24 25	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to X \in J$
27	23 26	elmapd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to (f \in (Y^{X}) \leftrightarrow f : X ⟶ Y)$
28		iscnp3	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \to (f \in (J CnP K) (A) \leftrightarrow (f : X ⟶ Y \land \forall x \in K (f (A) \in x \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x]))))$
29	28	adantr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to (f \in (J CnP K) (A) \leftrightarrow (f : X ⟶ Y \land \forall x \in K (f (A) \in x \to \exists y \in J (A \in y \land y \subseteq f^{-1} [x]))))$
30	20 27 29	3bitr4rd	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to (f \in (J CnP K) (A) \leftrightarrow f \in (Y^{X}))$
31	30	eqrdv	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land A \in X) \land \{A\} \in J) \to (J CnP K) (A) = Y^{X}$

Metamath Proof Explorer

Theorem cnpdis

Proof