Metamath Proof Explorer

Theorem segconeu

Description: Existential uniqueness version of segconeq . (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion segconeu 
|- ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> E! r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> N e. NN )
2 simpr2 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
3 simpr1 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
4 axsegcon 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) )
5 1 2 3 4 syl3anc 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> E. r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) )
6 simpl23 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) /\ ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) ) -> C =/= D )
7 simprl 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) /\ ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) ) -> ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) )
8 simprr 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) /\ ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) ) -> ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) )
9 6 7 8 3jca 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) /\ ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) ) -> ( C =/= D /\ ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) )
10 9 ex 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> ( ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) -> ( C =/= D /\ ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) ) )
11 simp1 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> N e. NN )
12 simp22r 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
13 simp21l 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
14 simp21r 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
15 simp22l 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
16 simp3l 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> r e. ( EE ` N ) )
17 simp3r 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> s e. ( EE ` N ) )
18 segconeq 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> ( ( C =/= D /\ ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) -> r = s ) )
19 11 12 13 14 15 16 17 18 syl133anc 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> ( ( C =/= D /\ ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) -> r = s ) )
20 10 19 syld 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> ( ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) -> r = s ) )
21 20 3expa 
 |-  ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) /\ ( r e. ( EE ` N ) /\ s e. ( EE ` N ) ) ) -> ( ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) -> r = s ) )
22 21 ralrimivva 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> A. r e. ( EE ` N ) A. s e. ( EE ` N ) ( ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) -> r = s ) )
23 opeq2 
 |-  ( r = s -> <. C , r >. = <. C , s >. )
24 23 breq2d 
 |-  ( r = s -> ( D Btwn <. C , r >. <-> D Btwn <. C , s >. ) )
25 opeq2 
 |-  ( r = s -> <. D , r >. = <. D , s >. )
26 25 breq1d 
 |-  ( r = s -> ( <. D , r >. Cgr <. A , B >. <-> <. D , s >. Cgr <. A , B >. ) )
27 24 26 anbi12d 
 |-  ( r = s -> ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) <-> ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) )
28 27 reu4 
 |-  ( E! r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) <-> ( E. r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ A. r e. ( EE ` N ) A. s e. ( EE ` N ) ( ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) /\ ( D Btwn <. C , s >. /\ <. D , s >. Cgr <. A , B >. ) ) -> r = s ) ) )
29 5 22 28 sylanbrc 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> E! r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) )