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 ( 𝜑 → ( 𝐹𝑋 ) ( 𝐹𝑌 ) )