Metamath Proof Explorer

Theorem pmltpclem2

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

Ref Expression
Hypotheses pmltpc.1 
|- ( ph -> F e. ( RR ^pm RR ) )
pmltpc.2 
|- ( ph -> A C_ dom F )
pmltpc.3 
|- ( ph -> U e. A )
pmltpc.4 
|- ( ph -> V e. A )
pmltpc.5 
|- ( ph -> W e. A )
pmltpc.6 
|- ( ph -> X e. A )
pmltpc.7 
|- ( ph -> U <_ V )
pmltpc.8 
|- ( ph -> W <_ X )
pmltpc.9 
|- ( ph -> -. ( F ` U ) <_ ( F ` V ) )
pmltpc.10 
|- ( ph -> -. ( F ` X ) <_ ( F ` W ) )
Assertion pmltpclem2 
|- ( ph -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmltpc.1 
 |-  ( ph -> F e. ( RR ^pm RR ) )
2 pmltpc.2 
 |-  ( ph -> A C_ dom F )
3 pmltpc.3 
 |-  ( ph -> U e. A )
4 pmltpc.4 
 |-  ( ph -> V e. A )
5 pmltpc.5 
 |-  ( ph -> W e. A )
6 pmltpc.6 
 |-  ( ph -> X e. A )
7 pmltpc.7 
 |-  ( ph -> U <_ V )
8 pmltpc.8 
 |-  ( ph -> W <_ X )
9 pmltpc.9 
 |-  ( ph -> -. ( F ` U ) <_ ( F ` V ) )
10 pmltpc.10 
 |-  ( ph -> -. ( F ` X ) <_ ( F ` W ) )
11 5 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> W e. A )
12 3 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> U e. A )
13 4 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> V e. A )
14 simpr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> W < U )
15 reex 
 |-  RR e. _V
16 15 15 elpm2 
 |-  ( F e. ( RR ^pm RR ) <-> ( F : dom F --> RR /\ dom F C_ RR ) )
17 1 16 sylib 
 |-  ( ph -> ( F : dom F --> RR /\ dom F C_ RR ) )
18 17 simprd 
 |-  ( ph -> dom F C_ RR )
19 2 3 sseldd 
 |-  ( ph -> U e. dom F )
20 18 19 sseldd 
 |-  ( ph -> U e. RR )
21 2 4 sseldd 
 |-  ( ph -> V e. dom F )
22 18 21 sseldd 
 |-  ( ph -> V e. RR )
23 17 simpld 
 |-  ( ph -> F : dom F --> RR )
24 23 21 ffvelrnd 
 |-  ( ph -> ( F ` V ) e. RR )
25 23 19 ffvelrnd 
 |-  ( ph -> ( F ` U ) e. RR )
26 24 25 ltnled 
 |-  ( ph -> ( ( F ` V ) < ( F ` U ) <-> -. ( F ` U ) <_ ( F ` V ) ) )
27 9 26 mpbird 
 |-  ( ph -> ( F ` V ) < ( F ` U ) )
28 24 27 gtned 
 |-  ( ph -> ( F ` U ) =/= ( F ` V ) )
29 fveq2 
 |-  ( V = U -> ( F ` V ) = ( F ` U ) )
30 29 eqcomd 
 |-  ( V = U -> ( F ` U ) = ( F ` V ) )
31 30 necon3i 
 |-  ( ( F ` U ) =/= ( F ` V ) -> V =/= U )
32 28 31 syl 
 |-  ( ph -> V =/= U )
33 20 22 7 32 leneltd 
 |-  ( ph -> U < V )
34 33 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> U < V )
35 simplr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> ( F ` W ) < ( F ` U ) )
36 27 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> ( F ` V ) < ( F ` U ) )
37 35 36 jca 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> ( ( F ` W ) < ( F ` U ) /\ ( F ` V ) < ( F ` U ) ) )
38 37 orcd 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> ( ( ( F ` W ) < ( F ` U ) /\ ( F ` V ) < ( F ` U ) ) \/ ( ( F ` U ) < ( F ` W ) /\ ( F ` U ) < ( F ` V ) ) ) )
39 11 12 13 14 34 38 pmltpclem1 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ W < U ) -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
40 3 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> U e. A )
41 5 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> W e. A )
42 6 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> X e. A )
43 20 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> U e. RR )
44 2 5 sseldd 
 |-  ( ph -> W e. dom F )
45 18 44 sseldd 
 |-  ( ph -> W e. RR )
46 45 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> W e. RR )
47 simpr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> U <_ W )
48 23 44 ffvelrnd 
 |-  ( ph -> ( F ` W ) e. RR )
49 48 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> ( F ` W ) e. RR )
50 simplr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> ( F ` W ) < ( F ` U ) )
51 49 50 gtned 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> ( F ` U ) =/= ( F ` W ) )
52 fveq2 
 |-  ( W = U -> ( F ` W ) = ( F ` U ) )
53 52 eqcomd 
 |-  ( W = U -> ( F ` U ) = ( F ` W ) )
54 53 necon3i 
 |-  ( ( F ` U ) =/= ( F ` W ) -> W =/= U )
55 51 54 syl 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> W =/= U )
56 43 46 47 55 leneltd 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> U < W )
57 2 6 sseldd 
 |-  ( ph -> X e. dom F )
58 18 57 sseldd 
 |-  ( ph -> X e. RR )
59 23 57 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. RR )
60 48 59 ltnled 
 |-  ( ph -> ( ( F ` W ) < ( F ` X ) <-> -. ( F ` X ) <_ ( F ` W ) ) )
61 10 60 mpbird 
 |-  ( ph -> ( F ` W ) < ( F ` X ) )
62 48 61 gtned 
 |-  ( ph -> ( F ` X ) =/= ( F ` W ) )
63 fveq2 
 |-  ( X = W -> ( F ` X ) = ( F ` W ) )
64 63 necon3i 
 |-  ( ( F ` X ) =/= ( F ` W ) -> X =/= W )
65 62 64 syl 
 |-  ( ph -> X =/= W )
66 45 58 8 65 leneltd 
 |-  ( ph -> W < X )
67 66 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> W < X )
68 61 ad2antrr 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> ( F ` W ) < ( F ` X ) )
69 50 68 jca 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> ( ( F ` W ) < ( F ` U ) /\ ( F ` W ) < ( F ` X ) ) )
70 69 olcd 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> ( ( ( F ` U ) < ( F ` W ) /\ ( F ` X ) < ( F ` W ) ) \/ ( ( F ` W ) < ( F ` U ) /\ ( F ` W ) < ( F ` X ) ) ) )
71 40 41 42 56 67 70 pmltpclem1 
 |-  ( ( ( ph /\ ( F ` W ) < ( F ` U ) ) /\ U <_ W ) -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
72 45 adantr 
 |-  ( ( ph /\ ( F ` W ) < ( F ` U ) ) -> W e. RR )
73 20 adantr 
 |-  ( ( ph /\ ( F ` W ) < ( F ` U ) ) -> U e. RR )
74 39 71 72 73 ltlecasei 
 |-  ( ( ph /\ ( F ` W ) < ( F ` U ) ) -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
75 3 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> U e. A )
76 4 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> V e. A )
77 6 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> X e. A )
78 33 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> U < V )
79 simpr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> V < X )
80 27 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> ( F ` V ) < ( F ` U ) )
81 24 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` V ) e. RR )
82 25 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` U ) e. RR )
83 59 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` X ) e. RR )
84 27 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` V ) < ( F ` U ) )
85 48 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` W ) e. RR )
86 simpr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` U ) <_ ( F ` W ) )
87 61 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` W ) < ( F ` X ) )
88 82 85 83 86 87 lelttrd 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` U ) < ( F ` X ) )
89 81 82 83 84 88 lttrd 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> ( F ` V ) < ( F ` X ) )
90 89 adantr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> ( F ` V ) < ( F ` X ) )
91 80 90 jca 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> ( ( F ` V ) < ( F ` U ) /\ ( F ` V ) < ( F ` X ) ) )
92 91 olcd 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> ( ( ( F ` U ) < ( F ` V ) /\ ( F ` X ) < ( F ` V ) ) \/ ( ( F ` V ) < ( F ` U ) /\ ( F ` V ) < ( F ` X ) ) ) )
93 75 76 77 78 79 92 pmltpclem1 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ V < X ) -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
94 5 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> W e. A )
95 6 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> X e. A )
96 4 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> V e. A )
97 66 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> W < X )
98 58 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> X e. RR )
99 22 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> V e. RR )
100 simpr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> X <_ V )
101 24 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> ( F ` V ) e. RR )
102 89 adantr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> ( F ` V ) < ( F ` X ) )
103 101 102 gtned 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> ( F ` X ) =/= ( F ` V ) )
104 fveq2 
 |-  ( V = X -> ( F ` V ) = ( F ` X ) )
105 104 eqcomd 
 |-  ( V = X -> ( F ` X ) = ( F ` V ) )
106 105 necon3i 
 |-  ( ( F ` X ) =/= ( F ` V ) -> V =/= X )
107 103 106 syl 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> V =/= X )
108 98 99 100 107 leneltd 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> X < V )
109 61 ad2antrr 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> ( F ` W ) < ( F ` X ) )
110 109 102 jca 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> ( ( F ` W ) < ( F ` X ) /\ ( F ` V ) < ( F ` X ) ) )
111 110 orcd 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> ( ( ( F ` W ) < ( F ` X ) /\ ( F ` V ) < ( F ` X ) ) \/ ( ( F ` X ) < ( F ` W ) /\ ( F ` X ) < ( F ` V ) ) ) )
112 94 95 96 97 108 111 pmltpclem1 
 |-  ( ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) /\ X <_ V ) -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
113 22 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> V e. RR )
114 58 adantr 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> X e. RR )
115 93 112 113 114 ltlecasei 
 |-  ( ( ph /\ ( F ` U ) <_ ( F ` W ) ) -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
116 74 115 48 25 ltlecasei 
 |-  ( ph -> E. a e. A E. b e. A E. c e. A ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )