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 cn B B


Step Hyp Ref Expression
1 df-cncf cn = a 𝒫 , b 𝒫 f b a | x a y + z + w a x w < z f x f w < y
2 1 elmpocl2 F : A cn B B 𝒫
3 2 elpwid F : A cn B B