Theorem cnmptc

Description: A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmptid.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
	cnmptc.k	$$⊢\phi \to K\in \mathrm{TopOn}\left(Y\right)$$
	cnmptc.p	$$⊢\phi \to P\in Y$$
Assertion	cnmptc	$$⊢\phi \to \left(x\in X⟼P\right)\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmptid.j	$$⊢\phi \to J\in \mathrm{TopOn}\left(X\right)$$
2		cnmptc.k	$$⊢\phi \to K\in \mathrm{TopOn}\left(Y\right)$$
3		cnmptc.p	$$⊢\phi \to P\in Y$$
4		fconstmpt	$$⊢X\times \left\{P\right\}=\left(x\in X⟼P\right)$$
5		cnconst2	$$⊢\left(J\in \mathrm{TopOn}\left(X\right)\wedge K\in \mathrm{TopOn}\left(Y\right)\wedge P\in Y\right)\to X\times \left\{P\right\}\in \left(J\mathrm{Cn}K\right)$$
6	1 2 3 5	syl3anc	$$⊢\phi \to X\times \left\{P\right\}\in \left(J\mathrm{Cn}K\right)$$
7	4 6	eqeltrrid	$$⊢\phi \to \left(x\in X⟼P\right)\in \left(J\mathrm{Cn}K\right)$$