Metamath Proof Explorer

Theorem cncfrss

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

		Ref	Expression
	Assertion	cncfrss	\|- ( F e. ( A -cn-> B ) -> A C_ CC )

Proof

Step	Hyp	Ref	Expression
1		df-cncf	\|- -cn-> = ( a e. ~P CC , b e. ~P CC \|-> { f e. ( b ^m a ) \| A. x e. a A. y e. RR+ E. z e. RR+ A. w e. a ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) } )
2	1	elmpocl1	\|- ( F e. ( A -cn-> B ) -> A e. ~P CC )
3	2	elpwid	\|- ( F e. ( A -cn-> B ) -> A C_ CC )

Step

Hyp

Ref

Expression

df-cncf

 |-  -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. y e. RR+ E. z e. RR+ A. w e. a ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) } )

elmpocl1

 |-  ( F e. ( A -cn-> B ) -> A e. ~P CC )

elpwid

 |-  ( F e. ( A -cn-> B ) -> A C_ CC )