Metamath Proof Explorer

Theorem cndis

Description: Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	cndis	$⊢ (A \in V \land J \in TopOn (X)) \to 𝒫 A Cn J = X^{A}$

Proof

Step	Hyp	Ref	Expression
1		cnvimass	$⊢ f^{-1} [x] \subseteq dom f$
2		fdm	$⊢ f : A ⟶ X \to dom f = A$
3	2	adantl	$⊢ ((A \in V \land J \in TopOn (X)) \land f : A ⟶ X) \to dom f = A$
4	1 3	sseqtrid	$⊢ ((A \in V \land J \in TopOn (X)) \land f : A ⟶ X) \to f^{-1} [x] \subseteq A$
5		elpw2g	$⊢ A \in V \to (f^{-1} [x] \in 𝒫 A \leftrightarrow f^{-1} [x] \subseteq A)$
6	5	ad2antrr	$⊢ ((A \in V \land J \in TopOn (X)) \land f : A ⟶ X) \to (f^{-1} [x] \in 𝒫 A \leftrightarrow f^{-1} [x] \subseteq A)$
7	4 6	mpbird	$⊢ ((A \in V \land J \in TopOn (X)) \land f : A ⟶ X) \to f^{-1} [x] \in 𝒫 A$
8	7	ralrimivw	$⊢ ((A \in V \land J \in TopOn (X)) \land f : A ⟶ X) \to \forall x \in J f^{-1} [x] \in 𝒫 A$
9	8	ex	$⊢ (A \in V \land J \in TopOn (X)) \to (f : A ⟶ X \to \forall x \in J f^{-1} [x] \in 𝒫 A)$
10	9	pm4.71d	$⊢ (A \in V \land J \in TopOn (X)) \to (f : A ⟶ X \leftrightarrow (f : A ⟶ X \land \forall x \in J f^{-1} [x] \in 𝒫 A))$
11		toponmax	$⊢ J \in TopOn (X) \to X \in J$
12		id	$⊢ A \in V \to A \in V$
13		elmapg	$⊢ (X \in J \land A \in V) \to (f \in (X^{A}) \leftrightarrow f : A ⟶ X)$
14	11 12 13	syl2anr	$⊢ (A \in V \land J \in TopOn (X)) \to (f \in (X^{A}) \leftrightarrow f : A ⟶ X)$
15		distopon	$⊢ A \in V \to 𝒫 A \in TopOn (A)$
16		iscn	$⊢ (𝒫 A \in TopOn (A) \land J \in TopOn (X)) \to (f \in (𝒫 A Cn J) \leftrightarrow (f : A ⟶ X \land \forall x \in J f^{-1} [x] \in 𝒫 A))$
17	15 16	sylan	$⊢ (A \in V \land J \in TopOn (X)) \to (f \in (𝒫 A Cn J) \leftrightarrow (f : A ⟶ X \land \forall x \in J f^{-1} [x] \in 𝒫 A))$
18	10 14 17	3bitr4rd	$⊢ (A \in V \land J \in TopOn (X)) \to (f \in (𝒫 A Cn J) \leftrightarrow f \in (X^{A}))$
19	18	eqrdv	$⊢ (A \in V \land J \in TopOn (X)) \to 𝒫 A Cn J = X^{A}$