Metamath Proof Explorer

Theorem axcontlem9

Description: Lemma for axcont . Given the separation assumption, all values of F over A are less than or equal to all values of F over B . (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypotheses axcontlem9.1 
|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
axcontlem9.2 
|- F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
Assertion axcontlem9 
|- ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A. n e. ( F " A ) A. m e. ( F " B ) n <_ m )

Proof

Step Hyp Ref Expression
1 axcontlem9.1 
 |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2 axcontlem9.2 
 |-  F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
3 simpll 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> N e. NN )
4 simprl1 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> Z e. ( EE ` N ) )
5 simplr1 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A C_ ( EE ` N ) )
6 simprl2 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> U e. A )
7 5 6 sseldd 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> U e. ( EE ` N ) )
8 simprr 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> Z =/= U )
9 1 2 axcontlem2 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )
10 3 4 7 8 9 syl31anc 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )
11 f1ofun 
 |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) -> Fun F )
12 fvelima 
 |-  ( ( Fun F /\ n e. ( F " A ) ) -> E. a e. A ( F ` a ) = n )
13 12 ex 
 |-  ( Fun F -> ( n e. ( F " A ) -> E. a e. A ( F ` a ) = n ) )
14 10 11 13 3syl 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( n e. ( F " A ) -> E. a e. A ( F ` a ) = n ) )
15 fvelima 
 |-  ( ( Fun F /\ m e. ( F " B ) ) -> E. b e. B ( F ` b ) = m )
16 15 ex 
 |-  ( Fun F -> ( m e. ( F " B ) -> E. b e. B ( F ` b ) = m ) )
17 10 11 16 3syl 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( m e. ( F " B ) -> E. b e. B ( F ` b ) = m ) )
18 reeanv 
 |-  ( E. a e. A E. b e. B ( ( F ` a ) = n /\ ( F ` b ) = m ) <-> ( E. a e. A ( F ` a ) = n /\ E. b e. B ( F ` b ) = m ) )
19 simplr3 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A. x e. A A. y e. B x Btwn <. Z , y >. )
20 breq1 
 |-  ( x = a -> ( x Btwn <. Z , y >. <-> a Btwn <. Z , y >. ) )
21 opeq2 
 |-  ( y = b -> <. Z , y >. = <. Z , b >. )
22 21 breq2d 
 |-  ( y = b -> ( a Btwn <. Z , y >. <-> a Btwn <. Z , b >. ) )
23 20 22 rspc2v 
 |-  ( ( a e. A /\ b e. B ) -> ( A. x e. A A. y e. B x Btwn <. Z , y >. -> a Btwn <. Z , b >. ) )
24 19 23 mpan9 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> a Btwn <. Z , b >. )
25 simplll 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> N e. NN )
26 4 adantr 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> Z e. ( EE ` N ) )
27 7 adantr 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> U e. ( EE ` N ) )
28 25 26 27 3jca 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) )
29 simplrr 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> Z =/= U )
30 1 axcontlem4 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A C_ D )
31 30 sseld 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( a e. A -> a e. D ) )
32 simpl 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) )
33 1 axcontlem3 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> B C_ D )
34 32 4 6 8 33 syl13anc 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> B C_ D )
35 34 sseld 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( b e. B -> b e. D ) )
36 31 35 anim12d 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( ( a e. A /\ b e. B ) -> ( a e. D /\ b e. D ) ) )
37 36 imp 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> ( a e. D /\ b e. D ) )
38 1 2 axcontlem7 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( a e. D /\ b e. D ) ) -> ( a Btwn <. Z , b >. <-> ( F ` a ) <_ ( F ` b ) ) )
39 28 29 37 38 syl21anc 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> ( a Btwn <. Z , b >. <-> ( F ` a ) <_ ( F ` b ) ) )
40 24 39 mpbid 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> ( F ` a ) <_ ( F ` b ) )
41 breq12 
 |-  ( ( ( F ` a ) = n /\ ( F ` b ) = m ) -> ( ( F ` a ) <_ ( F ` b ) <-> n <_ m ) )
42 40 41 syl5ibcom 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( a e. A /\ b e. B ) ) -> ( ( ( F ` a ) = n /\ ( F ` b ) = m ) -> n <_ m ) )
43 42 rexlimdvva 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( E. a e. A E. b e. B ( ( F ` a ) = n /\ ( F ` b ) = m ) -> n <_ m ) )
44 18 43 biimtrrid 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( ( E. a e. A ( F ` a ) = n /\ E. b e. B ( F ` b ) = m ) -> n <_ m ) )
45 14 17 44 syl2and 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> ( ( n e. ( F " A ) /\ m e. ( F " B ) ) -> n <_ m ) )
46 45 ralrimivv 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) -> A. n e. ( F " A ) A. m e. ( F " B ) n <_ m )