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

Metamath Proof Explorer

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 )