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 ⊢ 𝐴 = ( Base ‘ 𝑉 )
mntf.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion mntf ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 mntf.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
2 mntf.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
3 eqid ⊢ ( le ‘ 𝑉 ) = ( le ‘ 𝑉 )
4 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
5 1 2 3 4 ismnt ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
6 5 biimp3a ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ( le ‘ 𝑉 ) 𝑦 → ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑦 ) ) ) )
7 6 simpld ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )