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 𝑊 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )