Theorem cncfrss

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

	Ref	Expression
Assertion	cncfrss	$$⊢F:A\underset{cn}{⟶}B\to A\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-cncf	$$⊢\underset{cn}{⟶}=\left(a\in 𝒫ℂ,b\in 𝒫ℂ⟼\left\{f\in \left(b^a\right)|\forall x\in a\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in a\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}\right)$$
2	1	elmpocl1	$$⊢F:A\underset{cn}{⟶}B\to A\in 𝒫ℂ$$
3	2	elpwid	$$⊢F:A\underset{cn}{⟶}B\to A\subseteq ℂ$$