Theorem mntf

Description: A monotone function is a function. (Contributed by Thierry Arnoux, 24-Apr-2024)

	Ref	Expression
Hypotheses	mntf.1	|- A = ( Base ` V )
	mntf.2	|- B = ( Base ` W )
Assertion	mntf	|- ( ( V e. X /\ W e. Y /\ F e. ( V Monot W ) ) -> F : A --> B )

Proof

Step	Hyp	Ref	Expression
1		mntf.1	|- A = ( Base ` V )
2		mntf.2	|- B = ( Base ` W )
3		eqid	|- ( le ` V ) = ( le ` V )
4		eqid	|- ( le ` W ) = ( le ` W )
5	1 2 3 4	ismnt	|- ( ( V e. X /\ W e. Y ) -> ( F e. ( V Monot W ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) ) ) )
6	5	biimp3a	|- ( ( V e. X /\ W e. Y /\ F e. ( V Monot W ) ) -> ( F : A --> B /\ A. x e. A A. y e. A ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) ) )
7	6	simpld	|- ( ( V e. X /\ W e. Y /\ F e. ( V Monot W ) ) -> F : A --> B )