Theorem axcontlem11

Description: Lemma for axcont . Eliminate the hypotheses from axcontlem10 . (Contributed by Scott Fenton, 20-Jun-2013)

	Ref	Expression
Assertion	axcontlem11	|- ( ( ( 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		opeq2	|- ( q = p -> <. Z , q >. = <. Z , p >. )
2	1	breq2d	|- ( q = p -> ( U Btwn <. Z , q >. <-> U Btwn <. Z , p >. ) )
3		breq1	|- ( q = p -> ( q Btwn <. Z , U >. <-> p Btwn <. Z , U >. ) )
4	2 3	orbi12d	|- ( q = p -> ( ( U Btwn <. Z , q >. \/ q Btwn <. Z , U >. ) <-> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
5	4	cbvrabv	|- { q e. ( EE ` N ) | ( U Btwn <. Z , q >. \/ q Btwn <. Z , U >. ) } = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
6		eqid	|- { <. z , r >. | ( z e. { q e. ( EE ` N ) | ( U Btwn <. Z , q >. \/ q Btwn <. Z , U >. ) } /\ ( r e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( z ` j ) = ( ( ( 1 - r ) x. ( Z ` j ) ) + ( r x. ( U ` j ) ) ) ) ) } = { <. z , r >. | ( z e. { q e. ( EE ` N ) | ( U Btwn <. Z , q >. \/ q Btwn <. Z , U >. ) } /\ ( r e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( z ` j ) = ( ( ( 1 - r ) x. ( Z ` j ) ) + ( r x. ( U ` j ) ) ) ) ) }
7	6	axcontlem1	|- { <. z , r >. | ( z e. { q e. ( EE ` N ) | ( U Btwn <. Z , q >. \/ q Btwn <. Z , U >. ) } /\ ( r e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( z ` j ) = ( ( ( 1 - r ) x. ( Z ` j ) ) + ( r x. ( U ` j ) ) ) ) ) } = { <. x , t >. | ( x e. { q e. ( EE ` N ) | ( U Btwn <. Z , q >. \/ q Btwn <. Z , U >. ) } /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
8	5 7	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 >. )