Metamath Proof Explorer

Theorem pmltpc

Description: Any function on the reals is either increasing, decreasing, or has a triple of points in a vee formation. (This theorem was created on demand by Mario Carneiro for the 6PCM conference in Bialystok, 1-Jul-2014.) (Contributed by Mario Carneiro, 1-Jul-2014)

Ref Expression
Assertion pmltpc ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∨ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rexanali ⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
2 1 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
3 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
4 2 3 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
5 rexanali ⊢ ( ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ¬ ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
6 5 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ 𝐴 ¬ ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
7 rexnal ⊢ ( ∃ 𝑧 ∈ 𝐴 ¬ ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ¬ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
8 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ≤ 𝑤 ↔ 𝑥 ≤ 𝑤 ) )
9 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
10 9 breq2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
11 8 10 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ( 𝑥 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
12 breq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑥 ≤ 𝑤 ↔ 𝑥 ≤ 𝑦 ) )
13 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) )
14 13 breq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
15 12 14 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑥 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
16 11 15 cbvral2vw ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
17 7 16 xchbinx ⊢ ( ∃ 𝑧 ∈ 𝐴 ¬ ∀ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
18 6 17 bitri ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
19 4 18 anbi12i ⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
20 reeanv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) )
21 ioran ⊢ ( ¬ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ↔ ( ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
22 19 20 21 3bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ¬ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
23 reeanv ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) )
24 simplll ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) )
25 24 simpld ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
26 24 simprd ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝐴 ⊆ dom 𝐹 )
27 simpllr ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
28 27 simpld ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝑥 ∈ 𝐴 )
29 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝑦 ∈ 𝐴 )
30 27 simprd ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝑧 ∈ 𝐴 )
31 simplrr ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝑤 ∈ 𝐴 )
32 simprll ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝑥 ≤ 𝑦 )
33 simprrl ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → 𝑧 ≤ 𝑤 )
34 simprlr ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) )
35 simprrr ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) )
36 25 26 28 29 30 31 32 33 34 35 pmltpclem2 ⊢ ( ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
37 36 ex ⊢ ( ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
38 37 rexlimdvva ⊢ ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
39 23 38 biimtrrid ⊢ ( ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
40 39 rexlimdvva ⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 ∧ ¬ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ∃ 𝑤 ∈ 𝐴 ( 𝑧 ≤ 𝑤 ∧ ¬ ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
41 22 40 biimtrrid ⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) → ( ¬ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
42 41 orrd ⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ∨ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
43 df-3or ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∨ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ) ∨ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
44 42 43 sylibr ⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐴 ⊆ dom 𝐹 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∨ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∨ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )