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→ 𝐵 ) → 𝐴 ⊆ ℂ )