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

Metamath Proof Explorer

Theorem cnfdmsn

Description: A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion cnfdmsn ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) ∈ ( 𝒫 { 𝐴 } Cn 𝒫 { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 fmptsnxp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = ( { 𝐴 } × { 𝐵 } ) )
2 snex ⊢ { 𝐴 } ∈ V
3 distopon ⊢ ( { 𝐴 } ∈ V → 𝒫 { 𝐴 } ∈ ( TopOn ‘ { 𝐴 } ) )
4 2 3 mp1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 { 𝐴 } ∈ ( TopOn ‘ { 𝐴 } ) )
5 snex ⊢ { 𝐵 } ∈ V
6 distopon ⊢ ( { 𝐵 } ∈ V → 𝒫 { 𝐵 } ∈ ( TopOn ‘ { 𝐵 } ) )
7 5 6 mp1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 { 𝐵 } ∈ ( TopOn ‘ { 𝐵 } ) )
8 snidg ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐵 } )
9 8 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ { 𝐵 } )
10 cnconst2 ⊢ ( ( 𝒫 { 𝐴 } ∈ ( TopOn ‘ { 𝐴 } ) ∧ 𝒫 { 𝐵 } ∈ ( TopOn ‘ { 𝐵 } ) ∧ 𝐵 ∈ { 𝐵 } ) → ( { 𝐴 } × { 𝐵 } ) ∈ ( 𝒫 { 𝐴 } Cn 𝒫 { 𝐵 } ) )
11 4 7 9 10 syl3anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) ∈ ( 𝒫 { 𝐴 } Cn 𝒫 { 𝐵 } ) )
12 1 11 eqeltrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) ∈ ( 𝒫 { 𝐴 } Cn 𝒫 { 𝐵 } ) )