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

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 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐵 ∈ 𝑌 ∧ 𝐹 : 𝑋 ⟶ { 𝐵 } ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fconst2g ⊢ ( 𝐵 ∈ 𝑌 → ( 𝐹 : 𝑋 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝑋 × { 𝐵 } ) ) )
2 1 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝐹 : 𝑋 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝑋 × { 𝐵 } ) ) )
3 cnconst2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝑋 × { 𝐵 } ) ∈ ( 𝐽 Cn 𝐾 ) )
4 3 3expa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝑋 × { 𝐵 } ) ∈ ( 𝐽 Cn 𝐾 ) )
5 eleq1 ⊢ ( 𝐹 = ( 𝑋 × { 𝐵 } ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑋 × { 𝐵 } ) ∈ ( 𝐽 Cn 𝐾 ) ) )
6 4 5 syl5ibrcom ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝐹 = ( 𝑋 × { 𝐵 } ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) )
7 2 6 sylbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝐹 : 𝑋 ⟶ { 𝐵 } → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) )
8 7 impr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐵 ∈ 𝑌 ∧ 𝐹 : 𝑋 ⟶ { 𝐵 } ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )