Metamath Proof Explorer

Theorem pmltpclem1

Description: Lemma for pmltpc . (Contributed by Mario Carneiro, 1-Jul-2014)

Ref Expression
Hypotheses pmltpclem1.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
pmltpclem1.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
pmltpclem1.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
pmltpclem1.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
pmltpclem1.5 ⊢ ( 𝜑 → 𝐵 < 𝐶 )
pmltpclem1.6 ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐶 ) ) ) )
Assertion pmltpclem1 ( 𝜑 → ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 ∃ 𝑐 ∈ 𝑆 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmltpclem1.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
2 pmltpclem1.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
3 pmltpclem1.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
4 pmltpclem1.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 pmltpclem1.5 ⊢ ( 𝜑 → 𝐵 < 𝐶 )
6 pmltpclem1.6 ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐶 ) ) ) )
7 breq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 < 𝑏 ↔ 𝐴 < 𝑏 ) )
8 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) )
9 8 breq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ) )
10 9 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ) )
11 8 breq2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ) )
12 11 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ↔ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) )
13 10 12 orbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
14 7 13 3anbi13d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ↔ ( 𝐴 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
15 breq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 < 𝑏 ↔ 𝐴 < 𝐵 ) )
16 breq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 < 𝑐 ↔ 𝐵 < 𝑐 ) )
17 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝐵 ) )
18 17 breq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ) )
19 17 breq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ) )
20 18 19 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ) ) )
21 17 breq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ) )
22 17 breq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ) )
23 21 22 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ↔ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ) ) )
24 20 23 orbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
25 15 16 24 3anbi123d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ↔ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ) )
26 breq2 ⊢ ( 𝑐 = 𝐶 → ( 𝐵 < 𝑐 ↔ 𝐵 < 𝐶 ) )
27 fveq2 ⊢ ( 𝑐 = 𝐶 → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ 𝐶 ) )
28 27 breq1d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) )
29 28 anbi2d ⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) ) )
30 27 breq2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ↔ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐶 ) ) )
31 30 anbi2d ⊢ ( 𝑐 = 𝐶 → ( ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ) ↔ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐶 ) ) ) )
32 29 31 orbi12d ⊢ ( 𝑐 = 𝐶 → ( ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ) ) ↔ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐶 ) ) ) ) )
33 26 32 3anbi23d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) ↔ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ∧ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐶 ) ) ) ) ) )
34 14 25 33 rspc3ev ⊢ ( ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ∧ ( ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) ∨ ( ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐵 ) < ( 𝐹 ‘ 𝐶 ) ) ) ) ) → ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 ∃ 𝑐 ∈ 𝑆 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
35 1 2 3 4 5 6 34 syl33anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 ∃ 𝑐 ∈ 𝑆 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )