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	|- ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) -> ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` 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 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rexanali	|- ( E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) <-> -. A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
2	1	rexbii	|- ( E. x e. A E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) <-> E. x e. A -. A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
3		rexnal	|- ( E. x e. A -. A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) <-> -. A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
4	2 3	bitri	|- ( E. x e. A E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) <-> -. A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
5		rexanali	|- ( E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) <-> -. A. w e. A ( z <_ w -> ( F ` w ) <_ ( F ` z ) ) )
6	5	rexbii	|- ( E. z e. A E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) <-> E. z e. A -. A. w e. A ( z <_ w -> ( F ` w ) <_ ( F ` z ) ) )
7		rexnal	|- ( E. z e. A -. A. w e. A ( z <_ w -> ( F ` w ) <_ ( F ` z ) ) <-> -. A. z e. A A. w e. A ( z <_ w -> ( F ` w ) <_ ( F ` z ) ) )
8		breq1	|- ( z = x -> ( z <_ w <-> x <_ w ) )
9		fveq2	|- ( z = x -> ( F ` z ) = ( F ` x ) )
10	9	breq2d	|- ( z = x -> ( ( F ` w ) <_ ( F ` z ) <-> ( F ` w ) <_ ( F ` x ) ) )
11	8 10	imbi12d	|- ( z = x -> ( ( z <_ w -> ( F ` w ) <_ ( F ` z ) ) <-> ( x <_ w -> ( F ` w ) <_ ( F ` x ) ) ) )
12		breq2	|- ( w = y -> ( x <_ w <-> x <_ y ) )
13		fveq2	|- ( w = y -> ( F ` w ) = ( F ` y ) )
14	13	breq1d	|- ( w = y -> ( ( F ` w ) <_ ( F ` x ) <-> ( F ` y ) <_ ( F ` x ) ) )
15	12 14	imbi12d	|- ( w = y -> ( ( x <_ w -> ( F ` w ) <_ ( F ` x ) ) <-> ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) )
16	11 15	cbvral2vw	|- ( A. z e. A A. w e. A ( z <_ w -> ( F ` w ) <_ ( F ` z ) ) <-> A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
17	7 16	xchbinx	|- ( E. z e. A -. A. w e. A ( z <_ w -> ( F ` w ) <_ ( F ` z ) ) <-> -. A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
18	6 17	bitri	|- ( E. z e. A E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) <-> -. A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) )
19	4 18	anbi12i	|- ( ( E. x e. A E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ E. z e. A E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) <-> ( -. A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) /\ -. A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) )
20		reeanv	|- ( E. x e. A E. z e. A ( E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) <-> ( E. x e. A E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ E. z e. A E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) )
21		ioran	|- ( -. ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) <-> ( -. A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) /\ -. A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) )
22	19 20 21	3bitr4i	|- ( E. x e. A E. z e. A ( E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) <-> -. ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` x ) ) ) )
23		reeanv	|- ( E. y e. A E. w e. A ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) <-> ( E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) )
24		simplll	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> ( F e. ( RR ^pm RR ) /\ A C_ dom F ) )
25	24	simpld	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> F e. ( RR ^pm RR ) )
26	24	simprd	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> A C_ dom F )
27		simpllr	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> ( x e. A /\ z e. A ) )
28	27	simpld	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> x e. A )
29		simplrl	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> y e. A )
30	27	simprd	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> z e. A )
31		simplrr	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> w e. A )
32		simprll	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> x <_ y )
33		simprrl	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> z <_ w )
34		simprlr	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> -. ( F ` x ) <_ ( F ` y ) )
35		simprrr	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> -. ( F ` w ) <_ ( F ` z ) )
36	25 26 28 29 30 31 32 33 34 35	pmltpclem2	|- ( ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) /\ ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) ) -> 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 ) ) ) ) )
37	36	ex	|- ( ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) /\ ( y e. A /\ w e. A ) ) -> ( ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) -> 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 ) ) ) ) ) )
38	37	rexlimdvva	|- ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) -> ( E. y e. A E. w e. A ( ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) -> 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 ) ) ) ) ) )
39	23 38	biimtrrid	|- ( ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) /\ ( x e. A /\ z e. A ) ) -> ( ( E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) -> 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	39	rexlimdvva	|- ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) -> ( E. x e. A E. z e. A ( E. y e. A ( x <_ y /\ -. ( F ` x ) <_ ( F ` y ) ) /\ E. w e. A ( z <_ w /\ -. ( F ` w ) <_ ( F ` z ) ) ) -> 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 ) ) ) ) ) )
41	22 40	biimtrrid	|- ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) -> ( -. ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` 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 ) ) ) ) ) )
42	41	orrd	|- ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) -> ( ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` 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 ) ) ) ) ) )
43		df-3or	|- ( ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` 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 ) ) ) ) ) <-> ( ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` 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 ) ) ) ) ) )
44	42 43	sylibr	|- ( ( F e. ( RR ^pm RR ) /\ A C_ dom F ) -> ( A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) \/ A. x e. A A. y e. A ( x <_ y -> ( F ` y ) <_ ( F ` 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 ) ) ) ) ) )