This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncfrss2

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

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

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