Metamath Proof Explorer

Theorem brsegle

Description: Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion brsegle 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. A , B >. e. _V
2 opex 
 |-  <. C , D >. e. _V
3 eqeq1 
 |-  ( p = <. A , B >. -> ( p = <. a , b >. <-> <. A , B >. = <. a , b >. ) )
4 eqcom 
 |-  ( <. A , B >. = <. a , b >. <-> <. a , b >. = <. A , B >. )
5 3 4 bitrdi 
 |-  ( p = <. A , B >. -> ( p = <. a , b >. <-> <. a , b >. = <. A , B >. ) )
6 5 3anbi1d 
 |-  ( p = <. A , B >. -> ( ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
7 6 rexbidv 
 |-  ( p = <. A , B >. -> ( E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
8 7 2rexbidv 
 |-  ( p = <. A , B >. -> ( E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
9 8 2rexbidv 
 |-  ( p = <. A , B >. -> ( E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
10 eqeq1 
 |-  ( q = <. C , D >. -> ( q = <. c , d >. <-> <. C , D >. = <. c , d >. ) )
11 eqcom 
 |-  ( <. C , D >. = <. c , d >. <-> <. c , d >. = <. C , D >. )
12 10 11 bitrdi 
 |-  ( q = <. C , D >. -> ( q = <. c , d >. <-> <. c , d >. = <. C , D >. ) )
13 12 3anbi2d 
 |-  ( q = <. C , D >. -> ( ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
14 13 rexbidv 
 |-  ( q = <. C , D >. -> ( E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
15 14 2rexbidv 
 |-  ( q = <. C , D >. -> ( E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
16 15 2rexbidv 
 |-  ( q = <. C , D >. -> ( E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
17 df-segle 
 |-  Seg<_ = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) }
18 1 2 9 16 17 brab 
 |-  ( <. A , B >. Seg<_ <. C , D >. <-> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
19 vex 
 |-  a e. _V
20 vex 
 |-  b e. _V
21 19 20 opth 
 |-  ( <. a , b >. = <. A , B >. <-> ( a = A /\ b = B ) )
22 vex 
 |-  c e. _V
23 vex 
 |-  d e. _V
24 22 23 opth 
 |-  ( <. c , d >. = <. C , D >. <-> ( c = C /\ d = D ) )
25 biid 
 |-  ( E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) <-> E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) )
26 21 24 25 3anbi123i 
 |-  ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
27 26 2rexbii 
 |-  ( E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
28 27 2rexbii 
 |-  ( E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
29 28 rexbii 
 |-  ( E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
30 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) -> A e. ( EE ` N ) )
31 30 ad2antrl 
 |-  ( ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) /\ ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) -> A e. ( EE ` N ) )
32 eleenn 
 |-  ( A e. ( EE ` N ) -> N e. NN )
33 31 32 syl 
 |-  ( ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) /\ ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) -> N e. NN )
34 simprlr 
 |-  ( ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) /\ ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) -> n e. NN )
35 simprll 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) -> A e. ( EE ` n ) )
36 35 adantl 
 |-  ( ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) /\ ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) -> A e. ( EE ` n ) )
37 axdimuniq 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) ) /\ ( n e. NN /\ A e. ( EE ` n ) ) ) -> N = n )
38 33 31 34 36 37 syl22anc 
 |-  ( ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) /\ ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) -> N = n )
39 38 fveq2d 
 |-  ( ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) /\ ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) -> ( EE ` N ) = ( EE ` n ) )
40 39 rexeqdv 
 |-  ( ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) /\ ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) -> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) <-> E. y e. ( EE ` n ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
41 40 exbiri 
 |-  ( ( a = A /\ ( b = B /\ ( c = C /\ d = D ) ) ) -> ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) -> ( E. y e. ( EE ` n ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
42 41 anassrs 
 |-  ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) -> ( E. y e. ( EE ` n ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
43 eleq1 
 |-  ( a = A -> ( a e. ( EE ` n ) <-> A e. ( EE ` n ) ) )
44 eleq1 
 |-  ( b = B -> ( b e. ( EE ` n ) <-> B e. ( EE ` n ) ) )
45 43 44 bi2anan9 
 |-  ( ( a = A /\ b = B ) -> ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) <-> ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) ) )
46 eleq1 
 |-  ( c = C -> ( c e. ( EE ` n ) <-> C e. ( EE ` n ) ) )
47 eleq1 
 |-  ( d = D -> ( d e. ( EE ` n ) <-> D e. ( EE ` n ) ) )
48 46 47 bi2anan9 
 |-  ( ( c = C /\ d = D ) -> ( ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) <-> ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) )
49 45 48 bi2anan9 
 |-  ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) ) <-> ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) )
50 49 anbi2d 
 |-  ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) ) ) <-> ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) ) /\ ( C e. ( EE ` n ) /\ D e. ( EE ` n ) ) ) ) ) )
51 opeq12 
 |-  ( ( a = A /\ b = B ) -> <. a , b >. = <. A , B >. )
52 51 breq1d 
 |-  ( ( a = A /\ b = B ) -> ( <. a , b >. Cgr <. c , y >. <-> <. A , B >. Cgr <. c , y >. ) )
53 52 anbi2d 
 |-  ( ( a = A /\ b = B ) -> ( ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) <-> ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) )
54 opeq12 
 |-  ( ( c = C /\ d = D ) -> <. c , d >. = <. C , D >. )
55 54 breq2d 
 |-  ( ( c = C /\ d = D ) -> ( y Btwn <. c , d >. <-> y Btwn <. C , D >. ) )
56 opeq1 
 |-  ( c = C -> <. c , y >. = <. C , y >. )
57 56 breq2d 
 |-  ( c = C -> ( <. A , B >. Cgr <. c , y >. <-> <. A , B >. Cgr <. C , y >. ) )
58 57 adantr 
 |-  ( ( c = C /\ d = D ) -> ( <. A , B >. Cgr <. c , y >. <-> <. A , B >. Cgr <. C , y >. ) )
59 55 58 anbi12d 
 |-  ( ( c = C /\ d = D ) -> ( ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) <-> ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
60 53 59 sylan9bb 
 |-  ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) <-> ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
61 60 rexbidv 
 |-  ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) <-> E. y e. ( EE ` n ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
62 61 imbi1d 
 |-  ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( ( E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) <-> ( E. y e. ( EE ` n ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
63 42 50 62 3imtr4d 
 |-  ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) ) ) -> ( E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
64 63 com12 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) ) ) -> ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) ) -> ( E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
65 64 expd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) ) ) -> ( ( a = A /\ b = B ) -> ( ( c = C /\ d = D ) -> ( E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) ) )
66 65 3impd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) ) ) -> ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
67 66 expr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) ) -> ( ( c e. ( EE ` n ) /\ d e. ( EE ` n ) ) -> ( ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
68 67 rexlimdvv 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) /\ ( a e. ( EE ` n ) /\ b e. ( EE ` n ) ) ) -> ( E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
69 68 rexlimdvva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ n e. NN ) -> ( E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
70 69 rexlimdva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( ( a = A /\ b = B ) /\ ( c = C /\ d = D ) /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
71 29 70 biimtrid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
72 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> N e. NN )
73 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> A e. ( EE ` N ) )
74 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> B e. ( EE ` N ) )
75 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> C e. ( EE ` N ) )
76 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> D e. ( EE ` N ) )
77 eqidd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> <. A , B >. = <. A , B >. )
78 eqidd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> <. C , D >. = <. C , D >. )
79 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) )
80 opeq1 
 |-  ( c = C -> <. c , d >. = <. C , d >. )
81 80 eqeq1d 
 |-  ( c = C -> ( <. c , d >. = <. C , D >. <-> <. C , d >. = <. C , D >. ) )
82 80 breq2d 
 |-  ( c = C -> ( y Btwn <. c , d >. <-> y Btwn <. C , d >. ) )
83 82 57 anbi12d 
 |-  ( c = C -> ( ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) <-> ( y Btwn <. C , d >. /\ <. A , B >. Cgr <. C , y >. ) ) )
84 83 rexbidv 
 |-  ( c = C -> ( E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) <-> E. y e. ( EE ` N ) ( y Btwn <. C , d >. /\ <. A , B >. Cgr <. C , y >. ) ) )
85 81 84 3anbi23d 
 |-  ( c = C -> ( ( <. A , B >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) <-> ( <. A , B >. = <. A , B >. /\ <. C , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. C , d >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
86 opeq2 
 |-  ( d = D -> <. C , d >. = <. C , D >. )
87 86 eqeq1d 
 |-  ( d = D -> ( <. C , d >. = <. C , D >. <-> <. C , D >. = <. C , D >. ) )
88 86 breq2d 
 |-  ( d = D -> ( y Btwn <. C , d >. <-> y Btwn <. C , D >. ) )
89 88 anbi1d 
 |-  ( d = D -> ( ( y Btwn <. C , d >. /\ <. A , B >. Cgr <. C , y >. ) <-> ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
90 89 rexbidv 
 |-  ( d = D -> ( E. y e. ( EE ` N ) ( y Btwn <. C , d >. /\ <. A , B >. Cgr <. C , y >. ) <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
91 87 90 3anbi23d 
 |-  ( d = D -> ( ( <. A , B >. = <. A , B >. /\ <. C , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. C , d >. /\ <. A , B >. Cgr <. C , y >. ) ) <-> ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) )
92 85 91 rspc2ev 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ ( <. A , B >. = <. A , B >. /\ <. C , D >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) -> E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. A , B >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) )
93 75 76 77 78 79 92 syl113anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. A , B >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) )
94 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
95 94 eqeq1d 
 |-  ( a = A -> ( <. a , b >. = <. A , B >. <-> <. A , b >. = <. A , B >. ) )
96 94 breq1d 
 |-  ( a = A -> ( <. a , b >. Cgr <. c , y >. <-> <. A , b >. Cgr <. c , y >. ) )
97 96 anbi2d 
 |-  ( a = A -> ( ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) <-> ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) ) )
98 97 rexbidv 
 |-  ( a = A -> ( E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) <-> E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) ) )
99 95 98 3anbi13d 
 |-  ( a = A -> ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> ( <. A , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) ) ) )
100 99 2rexbidv 
 |-  ( a = A -> ( E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. A , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) ) ) )
101 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
102 101 eqeq1d 
 |-  ( b = B -> ( <. A , b >. = <. A , B >. <-> <. A , B >. = <. A , B >. ) )
103 101 breq1d 
 |-  ( b = B -> ( <. A , b >. Cgr <. c , y >. <-> <. A , B >. Cgr <. c , y >. ) )
104 103 anbi2d 
 |-  ( b = B -> ( ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) <-> ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) )
105 104 rexbidv 
 |-  ( b = B -> ( E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) <-> E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) )
106 102 105 3anbi13d 
 |-  ( b = B -> ( ( <. A , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) ) <-> ( <. A , B >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) ) )
107 106 2rexbidv 
 |-  ( b = B -> ( E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. A , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , b >. Cgr <. c , y >. ) ) <-> E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. A , B >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) ) )
108 100 107 rspc2ev 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. A , B >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. A , B >. Cgr <. c , y >. ) ) ) -> E. a e. ( EE ` N ) E. b e. ( EE ` N ) E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
109 73 74 93 108 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> E. a e. ( EE ` N ) E. b e. ( EE ` N ) E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
110 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
111 110 rexeqdv 
 |-  ( n = N -> ( E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) <-> E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
112 111 3anbi3d 
 |-  ( n = N -> ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
113 110 112 rexeqbidv 
 |-  ( n = N -> ( E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
114 110 113 rexeqbidv 
 |-  ( n = N -> ( E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
115 110 114 rexeqbidv 
 |-  ( n = N -> ( E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. b e. ( EE ` N ) E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
116 110 115 rexeqbidv 
 |-  ( n = N -> ( E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. a e. ( EE ` N ) E. b e. ( EE ` N ) E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
117 116 rspcev 
 |-  ( ( N e. NN /\ E. a e. ( EE ` N ) E. b e. ( EE ` N ) E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` N ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) -> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
118 72 109 117 syl2anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) )
119 118 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) ) )
120 71 119 impbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >. Cgr <. c , y >. ) ) <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
121 18 120 bitrid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )