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 \in X \land W \in Y \land F \in (V Monot W)) \to F : A ⟶ B$

Step	Hyp	Ref	Expression
1		mntf.1	$⊢ A = {Base}_{V}$
2		mntf.2	$⊢ B = {Base}_{W}$
3		eqid	$⊢ \leq_{V} = \leq_{V}$
4		eqid	$⊢ \leq_{W} = \leq_{W}$
5	1 2 3 4	ismnt	$⊢ (V \in X \land W \in Y) \to (F \in (V Monot W) \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in A (x \leq_{V} y \to F (x) \leq_{W} F (y))))$
6	5	biimp3a	$⊢ (V \in X \land W \in Y \land F \in (V Monot W)) \to (F : A ⟶ B \land \forall x \in A \forall y \in A (x \leq_{V} y \to F (x) \leq_{W} F (y)))$
7	6	simpld	$⊢ (V \in X \land W \in Y \land F \in (V Monot W)) \to F : A ⟶ B$

Metamath Proof Explorer