cnconst

Description: A constant function is continuous. (Contributed by FL, 15-Jan-2007) (Proof shortened by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	cnconst	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (B \in Y \land F : X ⟶ \{B\})) \to F \in (J Cn K)$

Step	Hyp	Ref	Expression
1		fconst2g	$⊢ B \in Y \to (F : X ⟶ \{B\} \leftrightarrow F = X \times \{B\})$
2	1	adantl	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land B \in Y) \to (F : X ⟶ \{B\} \leftrightarrow F = X \times \{B\})$
3		cnconst2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land B \in Y) \to X \times \{B\} \in (J Cn K)$
4	3	3expa	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land B \in Y) \to X \times \{B\} \in (J Cn K)$
5		eleq1	$⊢ F = X \times \{B\} \to (F \in (J Cn K) \leftrightarrow X \times \{B\} \in (J Cn K))$
6	4 5	syl5ibrcom	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land B \in Y) \to (F = X \times \{B\} \to F \in (J Cn K))$
7	2 6	sylbid	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land B \in Y) \to (F : X ⟶ \{B\} \to F \in (J Cn K))$
8	7	impr	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land (B \in Y \land F : X ⟶ \{B\})) \to F \in (J Cn K)$

Metamath Proof Explorer