This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → J ∈ TopOn ⁡ X
cnmptc.k ⊢ φ → K ∈ TopOn ⁡ Y
cnmptc.p ⊢ φ → P ∈ Y
Assertion cnmptc ⊢ φ → x ∈ X ⟼ P ∈ J Cn K

Proof

Step Hyp Ref Expression
1 cnmptid.j ⊢ φ → J ∈ TopOn ⁡ X
2 cnmptc.k ⊢ φ → K ∈ TopOn ⁡ Y
3 cnmptc.p ⊢ φ → P ∈ Y
4 fconstmpt ⊢ X × P = x ∈ X ⟼ P
5 cnconst2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ Y → X × P ∈ J Cn K
6 1 2 3 5 syl3anc ⊢ φ → X × P ∈ J Cn K
7 4 6 eqeltrrid ⊢ φ → x ∈ X ⟼ P ∈ J Cn K