Description: Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | cncfrss | ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐴 ⊆ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-cncf | ⊢ –cn→ = ( 𝑎 ∈ 𝒫 ℂ , 𝑏 ∈ 𝒫 ℂ ↦ { 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } ) | |
2 | 1 | elmpocl1 | ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐴 ∈ 𝒫 ℂ ) |
3 | 2 | elpwid | ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐴 ⊆ ℂ ) |