# Metamath Proof Explorer

## Theorem axcontlem10

Description: Lemma for axcont . Given a handful of assumptions, derive the conclusion of the final theorem. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypotheses axcontlem10.1
`|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }`
axcontlem10.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 axcontlem10
`|- ( ( ( 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. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )`

### Proof

Step Hyp Ref Expression
1 axcontlem10.1
` |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }`
2 axcontlem10.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 imassrn
` |-  ( F " A ) C_ ran F`
4 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 )`
5 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 ) )`
6 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 ) )`
7 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 )`
8 6 7 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 ) )`
9 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 )`
10 1 2 axcontlem2
` |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )`
11 4 5 8 9 10 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 ) )`
12 f1ofo
` |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) -> F : D -onto-> ( 0 [,) +oo ) )`
13 forn
` |-  ( F : D -onto-> ( 0 [,) +oo ) -> ran F = ( 0 [,) +oo ) )`
14 11 12 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 ) ) -> ran F = ( 0 [,) +oo ) )`
15 3 14 sseqtrid
` |-  ( ( ( 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 " A ) C_ ( 0 [,) +oo ) )`
16 rge0ssre
` |-  ( 0 [,) +oo ) C_ RR`
17 15 16 sstrdi
` |-  ( ( ( 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 " A ) C_ RR )`
18 imassrn
` |-  ( F " B ) C_ ran F`
19 18 14 sseqtrid
` |-  ( ( ( 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 " B ) C_ ( 0 [,) +oo ) )`
20 19 16 sstrdi
` |-  ( ( ( 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 " B ) C_ RR )`
21 1 2 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. m e. ( F " A ) A. n e. ( F " B ) m <_ n )`
22 dedekindle
` |-  ( ( ( F " A ) C_ RR /\ ( F " B ) C_ RR /\ A. m e. ( F " A ) A. n e. ( F " B ) m <_ n ) -> E. k e. RR A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) )`
23 17 20 21 22 syl3anc
` |-  ( ( ( 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. k e. RR A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) )`
24 simpr
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ k e. RR ) -> k e. RR )`
25 simprl3
` |-  ( ( ( 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 =/= (/) )`
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ k e. RR ) -> B =/= (/) )`
27 n0
` |-  ( B =/= (/) <-> E. b b e. B )`
28 26 27 sylib
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ k e. RR ) -> E. b b e. B )`
29 0red
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ ( k e. RR /\ b e. B ) ) -> 0 e. RR )`
30 f1of
` |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) -> F : D --> ( 0 [,) +oo ) )`
31 11 30 syl
` |-  ( ( ( 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 --> ( 0 [,) +oo ) )`
32 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 )`
33 32 7 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. D )`
34 31 33 ffvelrnd
` |-  ( ( ( 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 ` U ) e. ( 0 [,) +oo ) )`
35 16 34 sseldi
` |-  ( ( ( 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 ` U ) e. RR )`
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ ( k e. RR /\ b e. B ) ) -> ( F ` U ) e. RR )`
37 simprl
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ ( k e. RR /\ b e. B ) ) -> k e. RR )`
38 elrege0
` |-  ( ( F ` U ) e. ( 0 [,) +oo ) <-> ( ( F ` U ) e. RR /\ 0 <_ ( F ` U ) ) )`
39 38 simprbi
` |-  ( ( F ` U ) e. ( 0 [,) +oo ) -> 0 <_ ( F ` U ) )`
40 34 39 syl
` |-  ( ( ( 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 ) ) -> 0 <_ ( F ` U ) )`
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ ( k e. RR /\ b e. B ) ) -> 0 <_ ( F ` U ) )`
42 f1of1
` |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) -> F : D -1-1-> ( 0 [,) +oo ) )`
43 11 42 syl
` |-  ( ( ( 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-> ( 0 [,) +oo ) )`
44 f1elima
` |-  ( ( F : D -1-1-> ( 0 [,) +oo ) /\ U e. D /\ A C_ D ) -> ( ( F ` U ) e. ( F " A ) <-> U e. A ) )`
45 43 33 32 44 syl3anc
` |-  ( ( ( 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 ` U ) e. ( F " A ) <-> U e. A ) )`
46 7 45 mpbird
` |-  ( ( ( 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 ` U ) e. ( F " A ) )`
` |-  ( ( ( ( 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 ) ) /\ ( k e. RR /\ b e. B ) ) -> ( F ` U ) e. ( F " A ) )`
48 simpr
` |-  ( ( ( ( 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. B )`
` |-  ( ( ( ( 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 ) -> F : D -1-1-> ( 0 [,) +oo ) )`
50 simpl1
` |-  ( ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) -> Z e. ( EE ` N ) )`
51 simpl2
` |-  ( ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) -> U e. A )`
52 simpr
` |-  ( ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) -> Z =/= U )`
53 50 51 52 3jca
` |-  ( ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) -> ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) )`
54 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 )`
55 53 54 sylan2
` |-  ( ( ( 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 )`
56 55 sselda
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 C_ D )`
58 f1elima
` |-  ( ( F : D -1-1-> ( 0 [,) +oo ) /\ b e. D /\ B C_ D ) -> ( ( F ` b ) e. ( F " B ) <-> b e. B ) )`
59 49 56 57 58 syl3anc
` |-  ( ( ( ( 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 ) -> ( ( F ` b ) e. ( F " B ) <-> b e. B ) )`
60 48 59 mpbird
` |-  ( ( ( ( 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 ) -> ( F ` b ) e. ( F " B ) )`
` |-  ( ( ( ( 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 ) ) /\ ( k e. RR /\ b e. B ) ) -> ( F ` b ) e. ( F " B ) )`
62 47 61 jca
` |-  ( ( ( ( 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 ) ) /\ ( k e. RR /\ b e. B ) ) -> ( ( F ` U ) e. ( F " A ) /\ ( F ` b ) e. ( F " B ) ) )`
63 breq1
` |-  ( m = ( F ` U ) -> ( m <_ k <-> ( F ` U ) <_ k ) )`
64 63 anbi1d
` |-  ( m = ( F ` U ) -> ( ( m <_ k /\ k <_ n ) <-> ( ( F ` U ) <_ k /\ k <_ n ) ) )`
65 breq2
` |-  ( n = ( F ` b ) -> ( k <_ n <-> k <_ ( F ` b ) ) )`
66 65 anbi2d
` |-  ( n = ( F ` b ) -> ( ( ( F ` U ) <_ k /\ k <_ n ) <-> ( ( F ` U ) <_ k /\ k <_ ( F ` b ) ) ) )`
67 64 66 rspc2va
` |-  ( ( ( ( F ` U ) e. ( F " A ) /\ ( F ` b ) e. ( F " B ) ) /\ A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) -> ( ( F ` U ) <_ k /\ k <_ ( F ` b ) ) )`
68 62 67 sylan
` |-  ( ( ( ( ( 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 ) ) /\ ( k e. RR /\ b e. B ) ) /\ A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) -> ( ( F ` U ) <_ k /\ k <_ ( F ` b ) ) )`
69 68 an32s
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ ( k e. RR /\ b e. B ) ) -> ( ( F ` U ) <_ k /\ k <_ ( F ` b ) ) )`
70 69 simpld
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ ( k e. RR /\ b e. B ) ) -> ( F ` U ) <_ k )`
71 29 36 37 41 70 letrd
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ ( k e. RR /\ b e. B ) ) -> 0 <_ k )`
72 71 expr
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ k e. RR ) -> ( b e. B -> 0 <_ k ) )`
73 72 exlimdv
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ k e. RR ) -> ( E. b b e. B -> 0 <_ k ) )`
74 28 73 mpd
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ k e. RR ) -> 0 <_ k )`
75 elrege0
` |-  ( k e. ( 0 [,) +oo ) <-> ( k e. RR /\ 0 <_ k ) )`
76 24 74 75 sylanbrc
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) /\ k e. RR ) -> k e. ( 0 [,) +oo ) )`
77 76 ex
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) -> ( k e. RR -> k e. ( 0 [,) +oo ) ) )`
78 1 ssrab3
` |-  D C_ ( EE ` N )`
79 simpr
` |-  ( ( A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) -> k e. ( 0 [,) +oo ) )`
80 f1ocnvdm
` |-  ( ( F : D -1-1-onto-> ( 0 [,) +oo ) /\ k e. ( 0 [,) +oo ) ) -> ( `' F ` k ) e. D )`
81 11 79 80 syl2an
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) ) -> ( `' F ` k ) e. D )`
82 78 81 sseldi
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) ) -> ( `' F ` k ) e. ( EE ` N ) )`
83 4 5 8 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 ) ) -> ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) )`
84 83 9 jca
` |-  ( ( ( 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 /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ 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 >. ) ) /\ ( ( Z e. ( EE ` N ) /\ U e. A /\ B =/= (/) ) /\ Z =/= U ) ) /\ ( ( A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) )`
86 32 sselda
` |-  ( ( ( ( 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 ) ) /\ q e. A ) -> q e. D )`
` |-  ( ( ( ( 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 ) ) /\ ( q e. A /\ r e. B ) ) -> q e. D )`
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> q e. D )`
89 simplr
` |-  ( ( ( A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) -> k e. ( 0 [,) +oo ) )`
90 11 89 80 syl2an
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( `' F ` k ) e. D )`
91 55 sselda
` |-  ( ( ( ( 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 ) ) /\ r e. B ) -> r e. D )`
` |-  ( ( ( ( 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 ) ) /\ ( q e. A /\ r e. B ) ) -> r e. D )`
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> r e. D )`
94 88 90 93 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( q e. D /\ ( `' F ` k ) e. D /\ r e. D ) )`
95 85 94 jca
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( q e. D /\ ( `' F ` k ) e. D /\ r e. D ) ) )`
96 f1ofun
` |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) -> Fun F )`
97 11 96 syl
` |-  ( ( ( 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 ) ) -> Fun F )`
98 fdm
` |-  ( F : D --> ( 0 [,) +oo ) -> dom F = D )`
99 11 30 98 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 ) ) -> dom F = D )`
100 32 99 sseqtrrd
` |-  ( ( ( 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_ dom F )`
101 funfvima2
` |-  ( ( Fun F /\ A C_ dom F ) -> ( q e. A -> ( F ` q ) e. ( F " A ) ) )`
102 97 100 101 syl2anc
` |-  ( ( ( 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 ) ) -> ( q e. A -> ( F ` q ) e. ( F " A ) ) )`
103 55 99 sseqtrrd
` |-  ( ( ( 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_ dom F )`
104 funfvima2
` |-  ( ( Fun F /\ B C_ dom F ) -> ( r e. B -> ( F ` r ) e. ( F " B ) ) )`
105 97 103 104 syl2anc
` |-  ( ( ( 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 ) ) -> ( r e. B -> ( F ` r ) e. ( F " B ) ) )`
106 102 105 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 ) ) -> ( ( q e. A /\ r e. B ) -> ( ( F ` q ) e. ( F " A ) /\ ( F ` r ) e. ( F " B ) ) ) )`
107 106 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 ) ) /\ ( q e. A /\ r e. B ) ) -> ( ( F ` q ) e. ( F " A ) /\ ( F ` r ) e. ( F " B ) ) )`
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( F ` q ) e. ( F " A ) /\ ( F ` r ) e. ( F " B ) ) )`
109 simprll
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) )`
110 breq1
` |-  ( m = ( F ` q ) -> ( m <_ k <-> ( F ` q ) <_ k ) )`
111 110 anbi1d
` |-  ( m = ( F ` q ) -> ( ( m <_ k /\ k <_ n ) <-> ( ( F ` q ) <_ k /\ k <_ n ) ) )`
112 breq2
` |-  ( n = ( F ` r ) -> ( k <_ n <-> k <_ ( F ` r ) ) )`
113 112 anbi2d
` |-  ( n = ( F ` r ) -> ( ( ( F ` q ) <_ k /\ k <_ n ) <-> ( ( F ` q ) <_ k /\ k <_ ( F ` r ) ) ) )`
114 111 113 rspc2v
` |-  ( ( ( F ` q ) e. ( F " A ) /\ ( F ` r ) e. ( F " B ) ) -> ( A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) -> ( ( F ` q ) <_ k /\ k <_ ( F ` r ) ) ) )`
115 108 109 114 sylc
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( F ` q ) <_ k /\ k <_ ( F ` r ) ) )`
116 f1ocnvfv2
` |-  ( ( F : D -1-1-onto-> ( 0 [,) +oo ) /\ k e. ( 0 [,) +oo ) ) -> ( F ` ( `' F ` k ) ) = k )`
117 11 89 116 syl2an
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( F ` ( `' F ` k ) ) = k )`
118 117 breq2d
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( F ` q ) <_ ( F ` ( `' F ` k ) ) <-> ( F ` q ) <_ k ) )`
119 117 breq1d
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( F ` ( `' F ` k ) ) <_ ( F ` r ) <-> k <_ ( F ` r ) ) )`
120 118 119 anbi12d
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( ( F ` q ) <_ ( F ` ( `' F ` k ) ) /\ ( F ` ( `' F ` k ) ) <_ ( F ` r ) ) <-> ( ( F ` q ) <_ k /\ k <_ ( F ` r ) ) ) )`
121 115 120 mpbird
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( ( F ` q ) <_ ( F ` ( `' F ` k ) ) /\ ( F ` ( `' F ` k ) ) <_ ( F ` r ) ) )`
122 1 2 axcontlem8
` |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ ( q e. D /\ ( `' F ` k ) e. D /\ r e. D ) ) -> ( ( ( F ` q ) <_ ( F ` ( `' F ` k ) ) /\ ( F ` ( `' F ` k ) ) <_ ( F ` r ) ) -> ( `' F ` k ) Btwn <. q , r >. ) )`
123 95 121 122 sylc
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) /\ ( q e. A /\ r e. B ) ) ) -> ( `' F ` k ) Btwn <. q , r >. )`
124 123 anassrs
` |-  ( ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) ) /\ ( q e. A /\ r e. B ) ) -> ( `' F ` k ) Btwn <. q , r >. )`
125 124 ralrimivva
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) ) -> A. q e. A A. r e. B ( `' F ` k ) Btwn <. q , r >. )`
126 opeq1
` |-  ( q = x -> <. q , r >. = <. x , r >. )`
127 126 breq2d
` |-  ( q = x -> ( ( `' F ` k ) Btwn <. q , r >. <-> ( `' F ` k ) Btwn <. x , r >. ) )`
128 opeq2
` |-  ( r = y -> <. x , r >. = <. x , y >. )`
129 128 breq2d
` |-  ( r = y -> ( ( `' F ` k ) Btwn <. x , r >. <-> ( `' F ` k ) Btwn <. x , y >. ) )`
130 127 129 cbvral2vw
` |-  ( A. q e. A A. r e. B ( `' F ` k ) Btwn <. q , r >. <-> A. x e. A A. y e. B ( `' F ` k ) Btwn <. x , y >. )`
131 125 130 sylib
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) ) -> A. x e. A A. y e. B ( `' F ` k ) Btwn <. x , y >. )`
132 breq1
` |-  ( b = ( `' F ` k ) -> ( b Btwn <. x , y >. <-> ( `' F ` k ) Btwn <. x , y >. ) )`
133 132 2ralbidv
` |-  ( b = ( `' F ` k ) -> ( A. x e. A A. y e. B b Btwn <. x , y >. <-> A. x e. A A. y e. B ( `' F ` k ) Btwn <. x , y >. ) )`
134 133 rspcev
` |-  ( ( ( `' F ` k ) e. ( EE ` N ) /\ A. x e. A A. y e. B ( `' F ` k ) Btwn <. x , y >. ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )`
135 82 131 134 syl2anc
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) /\ k e. ( 0 [,) +oo ) ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )`
136 135 expr
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) -> ( k e. ( 0 [,) +oo ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )`
137 77 136 syld
` |-  ( ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) ) -> ( k e. RR -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )`
138 137 ex
` |-  ( ( ( 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. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) -> ( k e. RR -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) ) )`
139 138 com23
` |-  ( ( ( 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 ) ) -> ( k e. RR -> ( A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) ) )`
140 139 rexlimdv
` |-  ( ( ( 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. k e. RR A. m e. ( F " A ) A. n e. ( F " B ) ( m <_ k /\ k <_ n ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )`
141 23 140 mpd
` |-  ( ( ( 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. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )`