Theorem mntf

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

	Ref	Expression
Hypotheses	mntf.1	$$⊢A={\mathrm{Base}}_V$$
	mntf.2	$$⊢B={\mathrm{Base}}_W$$
Assertion	mntf	Could not format assertion : No typesetting found for |- ( ( V e. X /\ W e. Y /\ F e. ( V Monot W ) ) -> F : A --> B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mntf.1	$$⊢A={\mathrm{Base}}_V$$
2		mntf.2	$$⊢B={\mathrm{Base}}_W$$
3		eqid	$$⊢{\le }_V={\le }_V$$
4		eqid	$$⊢{\le }_W={\le }_W$$
5	1 2 3 4	ismnt	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-
6	5	biimp3a	Could not format ( ( 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 ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) with typecode |-
7	6	simpld	Could not format ( ( V e. X /\ W e. Y /\ F e. ( V Monot W ) ) -> F : A --> B ) : No typesetting found for |- ( ( V e. X /\ W e. Y /\ F e. ( V Monot W ) ) -> F : A --> B ) with typecode |-