Metamath Proof Explorer

Theorem 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 ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ B ∈ Y ∧ F : X ⟶ B → F ∈ J Cn K

Proof

Step Hyp Ref Expression
1 fconst2g ⊢ B ∈ Y → F : X ⟶ B ↔ F = X × B
2 1 adantl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ B ∈ Y → F : X ⟶ B ↔ F = X × B
3 cnconst2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ B ∈ Y → X × B ∈ J Cn K
4 3 3expa ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ B ∈ Y → X × B ∈ J Cn K
5 eleq1 ⊢ F = X × B → F ∈ J Cn K ↔ X × B ∈ J Cn K
6 4 5 syl5ibrcom ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ B ∈ Y → F = X × B → F ∈ J Cn K
7 2 6 sylbid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ B ∈ Y → F : X ⟶ B → F ∈ J Cn K
8 7 impr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ B ∈ Y ∧ F : X ⟶ B → F ∈ J Cn K