Metamath Proof Explorer


Theorem cncfrss

Description: Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion cncfrss ( 𝐹 ∈ ( 𝐴cn𝐵 ) → 𝐴 ⊆ ℂ )

Proof

Step Hyp Ref Expression
1 df-cncf cn→ = ( 𝑎 ∈ 𝒫 ℂ , 𝑏 ∈ 𝒫 ℂ ↦ { 𝑓 ∈ ( 𝑏m 𝑎 ) ∣ ∀ 𝑥𝑎𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤𝑎 ( ( abs ‘ ( 𝑥𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓𝑥 ) − ( 𝑓𝑤 ) ) ) < 𝑦 ) } )
2 1 elmpocl1 ( 𝐹 ∈ ( 𝐴cn𝐵 ) → 𝐴 ∈ 𝒫 ℂ )
3 2 elpwid ( 𝐹 ∈ ( 𝐴cn𝐵 ) → 𝐴 ⊆ ℂ )