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 𝒫 { 𝐵 } ) )