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 ⊢ A ∈ V ∧ B ∈ W → x ∈ A ⟼ B ∈ 𝒫 A Cn 𝒫 B

Proof

Step Hyp Ref Expression
1 fmptsnxp ⊢ A ∈ V ∧ B ∈ W → x ∈ A ⟼ B = A × B
2 snex ⊢ A ∈ V
3 distopon ⊢ A ∈ V → 𝒫 A ∈ TopOn ⁡ A
4 2 3 mp1i ⊢ A ∈ V ∧ B ∈ W → 𝒫 A ∈ TopOn ⁡ A
5 snex ⊢ B ∈ V
6 distopon ⊢ B ∈ V → 𝒫 B ∈ TopOn ⁡ B
7 5 6 mp1i ⊢ A ∈ V ∧ B ∈ W → 𝒫 B ∈ TopOn ⁡ B
8 snidg ⊢ B ∈ W → B ∈ B
9 8 adantl ⊢ A ∈ V ∧ B ∈ W → B ∈ B
10 cnconst2 ⊢ 𝒫 A ∈ TopOn ⁡ A ∧ 𝒫 B ∈ TopOn ⁡ B ∧ B ∈ B → A × B ∈ 𝒫 A Cn 𝒫 B
11 4 7 9 10 syl3anc ⊢ A ∈ V ∧ B ∈ W → A × B ∈ 𝒫 A Cn 𝒫 B
12 1 11 eqeltrd ⊢ A ∈ V ∧ B ∈ W → x ∈ A ⟼ B ∈ 𝒫 A Cn 𝒫 B