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 ∈ X ∧ W ∈ Y ∧ F ∈ 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 ⊢ ≤ V = ≤ V
4 eqid ⊢ ≤ W = ≤ W
5 1 2 3 4 ismnt ⊢ V ∈ X ∧ W ∈ Y → F ∈ V Monot W ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A x ≤ V y → F ⁡ x ≤ W F ⁡ y
6 5 biimp3a ⊢ V ∈ X ∧ W ∈ Y ∧ F ∈ V Monot W → F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A x ≤ V y → F ⁡ x ≤ W F ⁡ y
7 6 simpld ⊢ V ∈ X ∧ W ∈ Y ∧ F ∈ V Monot W → F : A ⟶ B