Metamath Proof Explorer

Theorem ismntd

Description: Property of being a monotone increasing function, deduction version. (Contributed by Thierry Arnoux, 24-Apr-2024)

Ref Expression
Hypotheses ismntd.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
ismntd.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
ismntd.3 ⊢ ≤ = ( le ‘ 𝑉 )
ismntd.4 ⊢ ≲ = ( le ‘ 𝑊 )
ismntd.5 ⊢ ( 𝜑 → 𝑉 ∈ 𝐶 )
ismntd.6 ⊢ ( 𝜑 → 𝑊 ∈ 𝐷 )
ismntd.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑉 Monot 𝑊 ) )
ismntd.8 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
ismntd.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
ismntd.10 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
Assertion ismntd ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ismntd.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
2 ismntd.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
3 ismntd.3 ⊢ ≤ = ( le ‘ 𝑉 )
4 ismntd.4 ⊢ ≲ = ( le ‘ 𝑊 )
5 ismntd.5 ⊢ ( 𝜑 → 𝑉 ∈ 𝐶 )
6 ismntd.6 ⊢ ( 𝜑 → 𝑊 ∈ 𝐷 )
7 ismntd.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑉 Monot 𝑊 ) )
8 ismntd.8 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
9 ismntd.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
10 ismntd.10 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
11 1 2 3 4 ismnt ⊢ ( ( 𝑉 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ) → ( 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) ) )
12 11 biimp3a ⊢ ( ( 𝑉 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
13 12 simprd ⊢ ( ( 𝑉 ∈ 𝐶 ∧ 𝑊 ∈ 𝐷 ∧ 𝐹 ∈ ( 𝑉 Monot 𝑊 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
14 5 6 7 13 syl3anc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
15 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦 ) )
16 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
17 16 breq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑦 ) ) )
18 15 17 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑋 ≤ 𝑦 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ) )
19 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌 ) )
20 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑌 ) )
21 20 breq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑌 ) ) )
22 19 21 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑦 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑋 ≤ 𝑌 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑌 ) ) ) )
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝐴 = 𝐴 )
24 18 22 8 23 9 rspc2vd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≲ ( 𝐹 ‘ 𝑦 ) ) → ( 𝑋 ≤ 𝑌 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑌 ) ) ) )
25 14 10 24 mp2d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≲ ( 𝐹 ‘ 𝑌 ) )