Metamath Proof Explorer

Theorem axcontlem12

Description: Lemma for axcont . Eliminate the trivial cases from the previous lemmas. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Assertion axcontlem12 
|- ( ( ( 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )

Proof

Step Hyp Ref Expression
1 rzal 
 |-  ( B = (/) -> A. y e. B Z Btwn <. x , y >. )
2 1 ralrimivw 
 |-  ( B = (/) -> A. x e. A A. y e. B Z Btwn <. x , y >. )
3 breq1 
 |-  ( b = Z -> ( b Btwn <. x , y >. <-> Z Btwn <. x , y >. ) )
4 3 2ralbidv 
 |-  ( b = Z -> ( A. x e. A A. y e. B b Btwn <. x , y >. <-> A. x e. A A. y e. B Z Btwn <. x , y >. ) )
5 4 rspcev 
 |-  ( ( Z e. ( EE ` N ) /\ A. x e. A A. y e. B Z Btwn <. x , y >. ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )
6 5 expcom 
 |-  ( A. x e. A A. y e. B Z Btwn <. x , y >. -> ( Z e. ( EE ` N ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
7 2 6 syl 
 |-  ( B = (/) -> ( Z e. ( EE ` N ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
8 7 adantld 
 |-  ( 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
9 8 adantld 
 |-  ( B = (/) -> ( ( ( u e. A /\ 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 ) ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
10 simprrl 
 |-  ( ( B =/= (/) /\ ( ( u e. A /\ 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 ) ) ) ) -> ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) )
11 simprrr 
 |-  ( ( B =/= (/) /\ ( ( u e. A /\ 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 ) ) ) ) -> Z e. ( EE ` N ) )
12 simprll 
 |-  ( ( B =/= (/) /\ ( ( u e. A /\ 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 )
13 simpl 
 |-  ( ( B =/= (/) /\ ( ( u e. A /\ 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 ) ) ) ) -> B =/= (/) )
14 11 12 13 3jca 
 |-  ( ( B =/= (/) /\ ( ( u e. A /\ 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 ) ) ) ) -> ( Z e. ( EE ` N ) /\ u e. A /\ B =/= (/) ) )
15 simprlr 
 |-  ( ( B =/= (/) /\ ( ( u e. A /\ 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 ) ) ) ) -> Z =/= u )
16 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 >. )
17 10 14 15 16 syl12anc 
 |-  ( ( B =/= (/) /\ ( ( u e. A /\ 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 ) ) ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )
18 17 ex 
 |-  ( B =/= (/) -> ( ( ( u e. A /\ 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 ) ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
19 9 18 pm2.61ine 
 |-  ( ( ( u e. A /\ 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 ) ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )
20 19 ex 
 |-  ( ( u e. A /\ 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
21 20 rexlimiva 
 |-  ( E. u e. A 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
22 df-ne 
 |-  ( Z =/= u <-> -. Z = u )
23 22 con2bii 
 |-  ( Z = u <-> -. Z =/= u )
24 23 ralbii 
 |-  ( A. u e. A Z = u <-> A. u e. A -. Z =/= u )
25 ralnex 
 |-  ( A. u e. A -. Z =/= u <-> -. E. u e. A Z =/= u )
26 24 25 bitri 
 |-  ( A. u e. A Z = u <-> -. E. u e. A Z =/= u )
27 simpr3 
 |-  ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) -> A. x e. A A. y e. B x Btwn <. Z , y >. )
28 eqeq2 
 |-  ( u = x -> ( Z = u <-> Z = x ) )
29 28 rspccva 
 |-  ( ( A. u e. A Z = u /\ x e. A ) -> Z = x )
30 opeq1 
 |-  ( Z = x -> <. Z , y >. = <. x , y >. )
31 30 breq2d 
 |-  ( Z = x -> ( x Btwn <. Z , y >. <-> x Btwn <. x , y >. ) )
32 breq1 
 |-  ( Z = x -> ( Z Btwn <. x , y >. <-> x Btwn <. x , y >. ) )
33 31 32 bitr4d 
 |-  ( Z = x -> ( x Btwn <. Z , y >. <-> Z Btwn <. x , y >. ) )
34 33 ralbidv 
 |-  ( Z = x -> ( A. y e. B x Btwn <. Z , y >. <-> A. y e. B Z Btwn <. x , y >. ) )
35 29 34 syl 
 |-  ( ( A. u e. A Z = u /\ x e. A ) -> ( A. y e. B x Btwn <. Z , y >. <-> A. y e. B Z Btwn <. x , y >. ) )
36 35 ralbidva 
 |-  ( A. u e. A Z = u -> ( A. x e. A A. y e. B x Btwn <. Z , y >. <-> A. x e. A A. y e. B Z Btwn <. x , y >. ) )
37 36 biimpa 
 |-  ( ( A. u e. A Z = u /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) -> A. x e. A A. y e. B Z Btwn <. x , y >. )
38 27 37 sylan2 
 |-  ( ( A. u e. A 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 >. ) ) ) -> A. x e. A A. y e. B Z Btwn <. x , y >. )
39 38 5 sylan2 
 |-  ( ( Z e. ( EE ` N ) /\ ( A. u e. A 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 >. ) ) ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )
40 39 ancoms 
 |-  ( ( ( A. u e. A 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )
41 40 expl 
 |-  ( A. u e. A 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
42 26 41 sylbir 
 |-  ( -. E. u e. A 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) )
43 21 42 pm2.61i 
 |-  ( ( ( 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 ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )