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 𝐾 ) )