MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eengtrkg Structured version   Unicode version

Theorem eengtrkg 24409
Description: The geometry structure for  EE ^ N is a Tarski geometry (Contributed by Thierry Arnoux, 15-Mar-2019.)
Assertion
Ref Expression
eengtrkg  |-  ( N  e.  NN  ->  (EEG `  N )  e. TarskiG )

Proof of Theorem eengtrkg
Dummy variables  a 
b  c  f  i  p  s  t  u  v  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5784 . . . . . . 7  |-  (EEG `  N )  e.  _V
21a1i 11 . . . . . 6  |-  ( N  e.  NN  ->  (EEG `  N )  e.  _V )
3 simpl 455 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  N  e.  NN )
4 simprl 754 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  x  e.  ( Base `  (EEG `  N
) ) )
5 eengbas 24405 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( EE `  N )  =  ( Base `  (EEG `  N ) ) )
65adantr 463 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
74, 6eleqtrrd 2473 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  x  e.  ( EE `  N ) )
8 simprr 755 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  y  e.  ( Base `  (EEG `  N
) ) )
98, 6eleqtrrd 2473 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  y  e.  ( EE `  N ) )
10 axcgrrflx 24338 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  x  e.  ( EE `  N )  /\  y  e.  ( EE `  N
) )  ->  <. x ,  y >.Cgr <. y ,  x >. )
113, 7, 9, 10syl3anc 1226 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  <. x ,  y >.Cgr <. y ,  x >. )
12 eqid 2382 . . . . . . . . 9  |-  ( Base `  (EEG `  N )
)  =  ( Base `  (EEG `  N )
)
13 eqid 2382 . . . . . . . . 9  |-  ( dist `  (EEG `  N )
)  =  ( dist `  (EEG `  N )
)
143, 12, 13, 4, 8, 8, 4ecgrtg 24407 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( <. x ,  y >.Cgr <. y ,  x >.  <->  ( x (
dist `  (EEG `  N
) ) y )  =  ( y (
dist `  (EEG `  N
) ) x ) ) )
1511, 14mpbid 210 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( x
( dist `  (EEG `  N
) ) y )  =  ( y (
dist `  (EEG `  N
) ) x ) )
1615ralrimivva 2803 . . . . . 6  |-  ( N  e.  NN  ->  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) ( x (
dist `  (EEG `  N
) ) y )  =  ( y (
dist `  (EEG `  N
) ) x ) )
17 simpl 455 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  ->  N  e.  NN )
18 simpr1 1000 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  ->  x  e.  ( Base `  (EEG `  N )
) )
19 simpr2 1001 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
y  e.  ( Base `  (EEG `  N )
) )
20 simpr3 1002 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
z  e.  ( Base `  (EEG `  N )
) )
2117, 12, 13, 18, 19, 20, 20ecgrtg 24407 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
( <. x ,  y
>.Cgr <. z ,  z
>. 
<->  ( x ( dist `  (EEG `  N )
) y )  =  ( z ( dist `  (EEG `  N )
) z ) ) )
2273adantr3 1155 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  ->  x  e.  ( EE `  N ) )
2393adantr3 1155 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
y  e.  ( EE
`  N ) )
245adantr 463 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
( EE `  N
)  =  ( Base `  (EEG `  N )
) )
2520, 24eleqtrrd 2473 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
z  e.  ( EE
`  N ) )
26 axcgrid 24340 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( EE `  N )  /\  y  e.  ( EE `  N )  /\  z  e.  ( EE `  N
) ) )  -> 
( <. x ,  y
>.Cgr <. z ,  z
>.  ->  x  =  y ) )
2717, 22, 23, 25, 26syl13anc 1228 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
( <. x ,  y
>.Cgr <. z ,  z
>.  ->  x  =  y ) )
2821, 27sylbird 235 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( x (
dist `  (EEG `  N
) ) y )  =  ( z (
dist `  (EEG `  N
) ) z )  ->  x  =  y ) )
2928ralrimivvva 2804 . . . . . 6  |-  ( N  e.  NN  ->  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) A. z  e.  ( Base `  (EEG `  N ) ) ( ( x ( dist `  (EEG `  N )
) y )  =  ( z ( dist `  (EEG `  N )
) z )  ->  x  =  y )
)
302, 16, 29jca32 533 . . . . 5  |-  ( N  e.  NN  ->  (
(EEG `  N )  e.  _V  /\  ( A. x  e.  ( Base `  (EEG `  N )
) A. y  e.  ( Base `  (EEG `  N ) ) ( x ( dist `  (EEG `  N ) ) y )  =  ( y ( dist `  (EEG `  N ) ) x )  /\  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) A. z  e.  ( Base `  (EEG `  N ) ) ( ( x ( dist `  (EEG `  N )
) y )  =  ( z ( dist `  (EEG `  N )
) z )  ->  x  =  y )
) ) )
31 eqid 2382 . . . . . 6  |-  (Itv `  (EEG `  N ) )  =  (Itv `  (EEG `  N ) )
3212, 13, 31istrkgc 23968 . . . . 5  |-  ( (EEG
`  N )  e. TarskiGC  <->  ( (EEG `  N )  e.  _V  /\  ( A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) ( x (
dist `  (EEG `  N
) ) y )  =  ( y (
dist `  (EEG `  N
) ) x )  /\  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) A. z  e.  ( Base `  (EEG `  N ) ) ( ( x ( dist `  (EEG `  N )
) y )  =  ( z ( dist `  (EEG `  N )
) z )  ->  x  =  y )
) ) )
3330, 32sylibr 212 . . . 4  |-  ( N  e.  NN  ->  (EEG `  N )  e. TarskiGC )
343, 12, 31, 4, 4, 8ebtwntg 24406 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  Btwn  <. x ,  x >.  <-> 
y  e.  ( x (Itv `  (EEG `  N
) ) x ) ) )
35 axbtwnid 24363 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  y  e.  ( EE `  N )  /\  x  e.  ( EE `  N
) )  ->  (
y  Btwn  <. x ,  x >.  ->  y  =  x ) )
363, 9, 7, 35syl3anc 1226 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  Btwn  <. x ,  x >.  ->  y  =  x ) )
3734, 36sylbird 235 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  e.  ( x (Itv `  (EEG `  N ) ) x )  ->  y  =  x ) )
3837imp 427 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  y  e.  ( x (Itv `  (EEG `  N ) ) x ) )  -> 
y  =  x )
3938eqcomd 2390 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  y  e.  ( x (Itv `  (EEG `  N ) ) x ) )  ->  x  =  y )
4039ex 432 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  e.  ( x (Itv `  (EEG `  N ) ) x )  ->  x  =  y ) )
4140ralrimivva 2803 . . . . . 6  |-  ( N  e.  NN  ->  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) ( y  e.  ( x (Itv `  (EEG `  N ) ) x )  ->  x  =  y ) )
42 simpll 751 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  N  e.  NN )
437adantr 463 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  x  e.  ( EE `  N ) )
449adantr 463 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  y  e.  ( EE `  N ) )
454adantr 463 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  x  e.  (
Base `  (EEG `  N
) ) )
468adantr 463 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  y  e.  (
Base `  (EEG `  N
) ) )
47 simpr1 1000 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  z  e.  (
Base `  (EEG `  N
) ) )
4842, 45, 46, 47, 25syl13anc 1228 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  z  e.  ( EE `  N ) )
49 simpr2 1001 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  u  e.  (
Base `  (EEG `  N
) ) )
5042, 5syl 16 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
5149, 50eleqtrrd 2473 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  u  e.  ( EE `  N ) )
52 simpr3 1002 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  v  e.  (
Base `  (EEG `  N
) ) )
5352, 50eleqtrrd 2473 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  v  e.  ( EE `  N ) )
54 axpasch 24365 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( EE `  N )  /\  y  e.  ( EE `  N )  /\  z  e.  ( EE `  N
) )  /\  (
u  e.  ( EE
`  N )  /\  v  e.  ( EE `  N ) ) )  ->  ( ( u 
Btwn  <. x ,  z
>.  /\  v  Btwn  <. y ,  z >. )  ->  E. a  e.  ( EE `  N ) ( a  Btwn  <. u ,  y >.  /\  a  Btwn  <. v ,  x >. ) ) )
5542, 43, 44, 48, 51, 53, 54syl132anc 1244 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  ( ( u 
Btwn  <. x ,  z
>.  /\  v  Btwn  <. y ,  z >. )  ->  E. a  e.  ( EE `  N ) ( a  Btwn  <. u ,  y >.  /\  a  Btwn  <. v ,  x >. ) ) )
5642, 12, 31, 45, 47, 49ebtwntg 24406 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  ( u  Btwn  <.
x ,  z >.  <->  u  e.  ( x (Itv
`  (EEG `  N
) ) z ) ) )
5742, 12, 31, 46, 47, 52ebtwntg 24406 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  ( v  Btwn  <.
y ,  z >.  <->  v  e.  ( y (Itv
`  (EEG `  N
) ) z ) ) )
5856, 57anbi12d 708 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  ( ( u 
Btwn  <. x ,  z
>.  /\  v  Btwn  <. y ,  z >. )  <->  ( u  e.  ( x (Itv `  (EEG `  N
) ) z )  /\  v  e.  ( y (Itv `  (EEG `  N ) ) z ) ) ) )
59 simplll 757 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  ->  N  e.  NN )
6049adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  ->  u  e.  ( Base `  (EEG `  N )
) )
6146adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
y  e.  ( Base `  (EEG `  N )
) )
62 simpr 459 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
a  e.  ( EE
`  N ) )
6350adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
( EE `  N
)  =  ( Base `  (EEG `  N )
) )
6462, 63eleqtrd 2472 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
a  e.  ( Base `  (EEG `  N )
) )
6559, 12, 31, 60, 61, 64ebtwntg 24406 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
( a  Btwn  <. u ,  y >.  <->  a  e.  ( u (Itv `  (EEG `  N ) ) y ) ) )
6652adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
v  e.  ( Base `  (EEG `  N )
) )
6745adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  ->  x  e.  ( Base `  (EEG `  N )
) )
6859, 12, 31, 66, 67, 64ebtwntg 24406 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
( a  Btwn  <. v ,  x >.  <->  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) )
6965, 68anbi12d 708 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  /\  a  e.  ( EE `  N ) )  -> 
( ( a  Btwn  <.
u ,  y >.  /\  a  Btwn  <. v ,  x >. )  <->  ( a  e.  ( u (Itv `  (EEG `  N ) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) ) )
7050, 69rexeqbidva 2996 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  ( E. a  e.  ( EE `  N
) ( a  Btwn  <.
u ,  y >.  /\  a  Btwn  <. v ,  x >. )  <->  E. a  e.  ( Base `  (EEG `  N ) ) ( a  e.  ( u (Itv `  (EEG `  N
) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) ) )
7155, 58, 703imtr3d 267 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  v  e.  ( Base `  (EEG `  N
) ) ) )  ->  ( ( u  e.  ( x (Itv
`  (EEG `  N
) ) z )  /\  v  e.  ( y (Itv `  (EEG `  N ) ) z ) )  ->  E. a  e.  ( Base `  (EEG `  N ) ) ( a  e.  ( u (Itv `  (EEG `  N
) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) ) )
7271ralrimivvva 2804 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  A. z  e.  ( Base `  (EEG `  N ) ) A. u  e.  ( Base `  (EEG `  N )
) A. v  e.  ( Base `  (EEG `  N ) ) ( ( u  e.  ( x (Itv `  (EEG `  N ) ) z )  /\  v  e.  ( y (Itv `  (EEG `  N ) ) z ) )  ->  E. a  e.  ( Base `  (EEG `  N
) ) ( a  e.  ( u (Itv
`  (EEG `  N
) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) ) )
7372ralrimivva 2803 . . . . . 6  |-  ( N  e.  NN  ->  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) A. z  e.  ( Base `  (EEG `  N ) ) A. u  e.  ( Base `  (EEG `  N )
) A. v  e.  ( Base `  (EEG `  N ) ) ( ( u  e.  ( x (Itv `  (EEG `  N ) ) z )  /\  v  e.  ( y (Itv `  (EEG `  N ) ) z ) )  ->  E. a  e.  ( Base `  (EEG `  N
) ) ( a  e.  ( u (Itv
`  (EEG `  N
) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) ) )
74 simpl 455 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  N  e.  NN )
75 elpwi 3936 . . . . . . . . . . 11  |-  ( s  e.  ~P ( Base `  (EEG `  N )
)  ->  s  C_  ( Base `  (EEG `  N
) ) )
7675ad2antrl 725 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  s  C_  ( Base `  (EEG `  N
) ) )
775adantr 463 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
7876, 77sseqtr4d 3454 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  s  C_  ( EE `  N ) )
79 elpwi 3936 . . . . . . . . . . 11  |-  ( t  e.  ~P ( Base `  (EEG `  N )
)  ->  t  C_  ( Base `  (EEG `  N
) ) )
8079ad2antll 726 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  t  C_  ( Base `  (EEG `  N
) ) )
8180, 77sseqtr4d 3454 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  t  C_  ( EE `  N ) )
82 simpll 751 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( s  C_  ( EE `  N )  /\  t  C_  ( EE `  N ) ) )  /\  E. a  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  x  Btwn  <. a ,  y >. )  ->  N  e.  NN )
83 simplrl 759 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( s  C_  ( EE `  N )  /\  t  C_  ( EE `  N ) ) )  /\  E. a  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  x  Btwn  <. a ,  y >. )  ->  s  C_  ( EE `  N ) )
84 simplrr 760 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( s  C_  ( EE `  N )  /\  t  C_  ( EE `  N ) ) )  /\  E. a  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  x  Btwn  <. a ,  y >. )  ->  t  C_  ( EE `  N ) )
85 simpr 459 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( s  C_  ( EE `  N )  /\  t  C_  ( EE `  N ) ) )  /\  E. a  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  x  Btwn  <. a ,  y >. )  ->  E. a  e.  ( EE `  N ) A. x  e.  s 
A. y  e.  t  x  Btwn  <. a ,  y >. )
86 axcont 24400 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( s  C_  ( EE `  N )  /\  t  C_  ( EE `  N )  /\  E. a  e.  ( EE `  N ) A. x  e.  s  A. y  e.  t  x  Btwn  <.
a ,  y >.
) )  ->  E. b  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  b  Btwn  <. x ,  y >. )
8782, 83, 84, 85, 86syl13anc 1228 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( s  C_  ( EE `  N )  /\  t  C_  ( EE `  N ) ) )  /\  E. a  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  x  Btwn  <. a ,  y >. )  ->  E. b  e.  ( EE `  N ) A. x  e.  s 
A. y  e.  t  b  Btwn  <. x ,  y >. )
8887ex 432 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( s  C_  ( EE `  N )  /\  t  C_  ( EE `  N ) ) )  ->  ( E. a  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  x  Btwn  <. a ,  y >.  ->  E. b  e.  ( EE `  N
) A. x  e.  s  A. y  e.  t  b  Btwn  <. x ,  y >. )
)
8974, 78, 81, 88syl12anc 1224 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  ( E. a  e.  ( EE `  N ) A. x  e.  s  A. y  e.  t  x  Btwn  <.
a ,  y >.  ->  E. b  e.  ( EE `  N ) A. x  e.  s 
A. y  e.  t  b  Btwn  <. x ,  y >. ) )
90 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  N  e.  NN )
91 simplr 753 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  a  e.  ( EE `  N ) )
9277ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
9391, 92eleqtrd 2472 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  a  e.  ( Base `  (EEG `  N
) ) )
9480ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  t  C_  ( Base `  (EEG `  N
) ) )
95 simprr 755 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  y  e.  t )
9694, 95sseldd 3418 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  y  e.  ( Base `  (EEG `  N
) ) )
9776ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  s  C_  ( Base `  (EEG `  N
) ) )
98 simprl 754 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  x  e.  s )
9997, 98sseldd 3418 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  x  e.  ( Base `  (EEG `  N
) ) )
10090, 12, 31, 93, 96, 99ebtwntg 24406 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  ( x  Btwn  <. a ,  y
>. 
<->  x  e.  ( a (Itv `  (EEG `  N
) ) y ) ) )
1011002ralbidva 2824 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  a  e.  ( EE `  N
) )  ->  ( A. x  e.  s  A. y  e.  t  x  Btwn  <. a ,  y
>. 
<-> 
A. x  e.  s 
A. y  e.  t  x  e.  ( a (Itv `  (EEG `  N
) ) y ) ) )
10277, 101rexeqbidva 2996 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  ( E. a  e.  ( EE `  N ) A. x  e.  s  A. y  e.  t  x  Btwn  <.
a ,  y >.  <->  E. a  e.  ( Base `  (EEG `  N )
) A. x  e.  s  A. y  e.  t  x  e.  ( a (Itv `  (EEG `  N ) ) y ) ) )
103 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  N  e.  NN )
10476ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  s  C_  ( Base `  (EEG `  N
) ) )
105 simprl 754 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  x  e.  s )
106104, 105sseldd 3418 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  x  e.  ( Base `  (EEG `  N
) ) )
10780ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  t  C_  ( Base `  (EEG `  N
) ) )
108 simprr 755 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  y  e.  t )
109107, 108sseldd 3418 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  y  e.  ( Base `  (EEG `  N
) ) )
110 simplr 753 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  b  e.  ( EE `  N ) )
11177ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
112110, 111eleqtrd 2472 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  b  e.  ( Base `  (EEG `  N
) ) )
113103, 12, 31, 106, 109, 112ebtwntg 24406 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N )
)  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  /\  (
x  e.  s  /\  y  e.  t )
)  ->  ( b  Btwn  <. x ,  y
>. 
<->  b  e.  ( x (Itv `  (EEG `  N
) ) y ) ) )
1141132ralbidva 2824 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  /\  b  e.  ( EE `  N
) )  ->  ( A. x  e.  s  A. y  e.  t 
b  Btwn  <. x ,  y >.  <->  A. x  e.  s 
A. y  e.  t  b  e.  ( x (Itv `  (EEG `  N
) ) y ) ) )
11577, 114rexeqbidva 2996 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  ( E. b  e.  ( EE `  N ) A. x  e.  s  A. y  e.  t  b  Btwn  <.
x ,  y >.  <->  E. b  e.  ( Base `  (EEG `  N )
) A. x  e.  s  A. y  e.  t  b  e.  ( x (Itv `  (EEG `  N ) ) y ) ) )
11689, 102, 1153imtr3d 267 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  ( E. a  e.  ( Base `  (EEG `  N )
) A. x  e.  s  A. y  e.  t  x  e.  ( a (Itv `  (EEG `  N ) ) y )  ->  E. b  e.  ( Base `  (EEG `  N ) ) A. x  e.  s  A. y  e.  t  b  e.  ( x (Itv `  (EEG `  N ) ) y ) ) )
117116ralrimivva 2803 . . . . . 6  |-  ( N  e.  NN  ->  A. s  e.  ~P  ( Base `  (EEG `  N ) ) A. t  e.  ~P  ( Base `  (EEG `  N
) ) ( E. a  e.  ( Base `  (EEG `  N )
) A. x  e.  s  A. y  e.  t  x  e.  ( a (Itv `  (EEG `  N ) ) y )  ->  E. b  e.  ( Base `  (EEG `  N ) ) A. x  e.  s  A. y  e.  t  b  e.  ( x (Itv `  (EEG `  N ) ) y ) ) )
11841, 73, 1173jca 1174 . . . . 5  |-  ( N  e.  NN  ->  ( A. x  e.  ( Base `  (EEG `  N
) ) A. y  e.  ( Base `  (EEG `  N ) ) ( y  e.  ( x (Itv `  (EEG `  N
) ) x )  ->  x  =  y )  /\  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) A. z  e.  ( Base `  (EEG `  N ) ) A. u  e.  ( Base `  (EEG `  N )
) A. v  e.  ( Base `  (EEG `  N ) ) ( ( u  e.  ( x (Itv `  (EEG `  N ) ) z )  /\  v  e.  ( y (Itv `  (EEG `  N ) ) z ) )  ->  E. a  e.  ( Base `  (EEG `  N
) ) ( a  e.  ( u (Itv
`  (EEG `  N
) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) )  /\  A. s  e.  ~P  ( Base `  (EEG `  N
) ) A. t  e.  ~P  ( Base `  (EEG `  N ) ) ( E. a  e.  (
Base `  (EEG `  N
) ) A. x  e.  s  A. y  e.  t  x  e.  ( a (Itv `  (EEG `  N ) ) y )  ->  E. b  e.  ( Base `  (EEG `  N ) ) A. x  e.  s  A. y  e.  t  b  e.  ( x (Itv `  (EEG `  N ) ) y ) ) ) )
11912, 13, 31istrkgb 23969 . . . . 5  |-  ( (EEG
`  N )  e. TarskiGB  <->  ( (EEG `  N )  e.  _V  /\  ( A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) ( y  e.  ( x (Itv `  (EEG `  N ) ) x )  ->  x  =  y )  /\  A. x  e.  ( Base `  (EEG `  N )
) A. y  e.  ( Base `  (EEG `  N ) ) A. z  e.  ( Base `  (EEG `  N )
) A. u  e.  ( Base `  (EEG `  N ) ) A. v  e.  ( Base `  (EEG `  N )
) ( ( u  e.  ( x (Itv
`  (EEG `  N
) ) z )  /\  v  e.  ( y (Itv `  (EEG `  N ) ) z ) )  ->  E. a  e.  ( Base `  (EEG `  N ) ) ( a  e.  ( u (Itv `  (EEG `  N
) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) )  /\  A. s  e.  ~P  ( Base `  (EEG `  N
) ) A. t  e.  ~P  ( Base `  (EEG `  N ) ) ( E. a  e.  (
Base `  (EEG `  N
) ) A. x  e.  s  A. y  e.  t  x  e.  ( a (Itv `  (EEG `  N ) ) y )  ->  E. b  e.  ( Base `  (EEG `  N ) ) A. x  e.  s  A. y  e.  t  b  e.  ( x (Itv `  (EEG `  N ) ) y ) ) ) ) )
1202, 118, 119sylanbrc 662 . . . 4  |-  ( N  e.  NN  ->  (EEG `  N )  e. TarskiGB )
12133, 120elind 3602 . . 3  |-  ( N  e.  NN  ->  (EEG `  N )  e.  (TarskiGC  i^i TarskiGB ) )
122 simplll 757 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  ->  N  e.  NN )
1234ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  ->  x  e.  ( Base `  (EEG `  N )
) )
124122, 5syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( EE `  N
)  =  ( Base `  (EEG `  N )
) )
125123, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  ->  x  e.  ( EE `  N ) )
1268ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
y  e.  ( Base `  (EEG `  N )
) )
127126, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
y  e.  ( EE
`  N ) )
128 simplr1 1036 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
z  e.  ( Base `  (EEG `  N )
) )
129128, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
z  e.  ( EE
`  N ) )
130 simplr2 1037 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  ->  u  e.  ( Base `  (EEG `  N )
) )
131130, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  ->  u  e.  ( EE `  N ) )
132 simplr3 1038 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
a  e.  ( Base `  (EEG `  N )
) )
133132, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
a  e.  ( EE
`  N ) )
134 simpr1 1000 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
b  e.  ( Base `  (EEG `  N )
) )
135134, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
b  e.  ( EE
`  N ) )
136 simpr2 1001 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
c  e.  ( Base `  (EEG `  N )
) )
137136, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
c  e.  ( EE
`  N ) )
138 simpr3 1002 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
v  e.  ( Base `  (EEG `  N )
) )
139138, 124eleqtrrd 2473 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
v  e.  ( EE
`  N ) )
140 3anass 975 . . . . . . . . . . . 12  |-  ( ( ( x  =/=  y  /\  y  Btwn  <. x ,  z >.  /\  b  Btwn  <. a ,  c
>. )  /\  ( <. x ,  y >.Cgr <. a ,  b >.  /\  <. y ,  z
>.Cgr <. b ,  c
>. )  /\  ( <. x ,  u >.Cgr <.
a ,  v >.  /\  <. y ,  u >.Cgr
<. b ,  v >.
) )  <->  ( (
x  =/=  y  /\  y  Btwn  <. x ,  z
>.  /\  b  Btwn  <. a ,  c >. )  /\  ( ( <. x ,  y >.Cgr <. a ,  b >.  /\  <. y ,  z >.Cgr <. b ,  c >. )  /\  ( <. x ,  u >.Cgr
<. a ,  v >.  /\  <. y ,  u >.Cgr
<. b ,  v >.
) ) ) )
141 ax5seg 24362 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  x  e.  ( EE
`  N )  /\  y  e.  ( EE `  N ) )  /\  ( z  e.  ( EE `  N )  /\  u  e.  ( EE `  N )  /\  a  e.  ( EE `  N ) )  /\  ( b  e.  ( EE `  N )  /\  c  e.  ( EE `  N
)  /\  v  e.  ( EE `  N ) ) )  ->  (
( ( x  =/=  y  /\  y  Btwn  <.
x ,  z >.  /\  b  Btwn  <. a ,  c >. )  /\  ( <. x ,  y
>.Cgr <. a ,  b
>.  /\  <. y ,  z
>.Cgr <. b ,  c
>. )  /\  ( <. x ,  u >.Cgr <.
a ,  v >.  /\  <. y ,  u >.Cgr
<. b ,  v >.
) )  ->  <. z ,  u >.Cgr <. c ,  v
>. ) )
142140, 141syl5bir 218 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  x  e.  ( EE
`  N )  /\  y  e.  ( EE `  N ) )  /\  ( z  e.  ( EE `  N )  /\  u  e.  ( EE `  N )  /\  a  e.  ( EE `  N ) )  /\  ( b  e.  ( EE `  N )  /\  c  e.  ( EE `  N
)  /\  v  e.  ( EE `  N ) ) )  ->  (
( ( x  =/=  y  /\  y  Btwn  <.
x ,  z >.  /\  b  Btwn  <. a ,  c >. )  /\  ( ( <. x ,  y >.Cgr <. a ,  b >.  /\  <. y ,  z >.Cgr <. b ,  c >. )  /\  ( <. x ,  u >.Cgr
<. a ,  v >.  /\  <. y ,  u >.Cgr
<. b ,  v >.
) ) )  ->  <. z ,  u >.Cgr <.
c ,  v >.
) )
143122, 125, 127, 129, 131, 133, 135, 137, 139, 142syl333anc 1258 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( ( x  =/=  y  /\  y  Btwn  <. x ,  z
>.  /\  b  Btwn  <. a ,  c >. )  /\  ( ( <. x ,  y >.Cgr <. a ,  b >.  /\  <. y ,  z >.Cgr <. b ,  c >. )  /\  ( <. x ,  u >.Cgr
<. a ,  v >.  /\  <. y ,  u >.Cgr
<. b ,  v >.
) ) )  ->  <. z ,  u >.Cgr <.
c ,  v >.
) )
144122, 12, 31, 123, 128, 126ebtwntg 24406 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( y  Btwn  <. x ,  z >.  <->  y  e.  ( x (Itv `  (EEG `  N ) ) z ) ) )
145122, 12, 31, 132, 136, 134ebtwntg 24406 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( b  Btwn  <. a ,  c >.  <->  b  e.  ( a (Itv `  (EEG `  N ) ) c ) ) )
146144, 1453anbi23d 1300 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( x  =/=  y  /\  y  Btwn  <.
x ,  z >.  /\  b  Btwn  <. a ,  c >. )  <->  ( x  =/=  y  /\  y  e.  ( x
(Itv `  (EEG `  N
) ) z )  /\  b  e.  ( a (Itv `  (EEG `  N ) ) c ) ) ) )
147122, 12, 13, 123, 126, 132, 134ecgrtg 24407 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( <. x ,  y
>.Cgr <. a ,  b
>. 
<->  ( x ( dist `  (EEG `  N )
) y )  =  ( a ( dist `  (EEG `  N )
) b ) ) )
148122, 12, 13, 126, 128, 134, 136ecgrtg 24407 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( <. y ,  z
>.Cgr <. b ,  c
>. 
<->  ( y ( dist `  (EEG `  N )
) z )  =  ( b ( dist `  (EEG `  N )
) c ) ) )
149147, 148anbi12d 708 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( <. x ,  y >.Cgr <. a ,  b >.  /\  <. y ,  z >.Cgr <. b ,  c >. )  <->  ( ( x ( dist `  (EEG `  N )
) y )  =  ( a ( dist `  (EEG `  N )
) b )  /\  ( y ( dist `  (EEG `  N )
) z )  =  ( b ( dist `  (EEG `  N )
) c ) ) ) )
150122, 12, 13, 123, 130, 132, 138ecgrtg 24407 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( <. x ,  u >.Cgr
<. a ,  v >.  <->  ( x ( dist `  (EEG `  N ) ) u )  =  ( a ( dist `  (EEG `  N ) ) v ) ) )
151122, 12, 13, 126, 130, 134, 138ecgrtg 24407 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( <. y ,  u >.Cgr
<. b ,  v >.  <->  ( y ( dist `  (EEG `  N ) ) u )  =  ( b ( dist `  (EEG `  N ) ) v ) ) )
152150, 151anbi12d 708 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( <. x ,  u >.Cgr <. a ,  v
>.  /\  <. y ,  u >.Cgr
<. b ,  v >.
)  <->  ( ( x ( dist `  (EEG `  N ) ) u )  =  ( a ( dist `  (EEG `  N ) ) v )  /\  ( y ( dist `  (EEG `  N ) ) u )  =  ( b ( dist `  (EEG `  N ) ) v ) ) ) )
153149, 152anbi12d 708 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( ( <.
x ,  y >.Cgr <. a ,  b >.  /\  <. y ,  z
>.Cgr <. b ,  c
>. )  /\  ( <. x ,  u >.Cgr <.
a ,  v >.  /\  <. y ,  u >.Cgr
<. b ,  v >.
) )  <->  ( (
( x ( dist `  (EEG `  N )
) y )  =  ( a ( dist `  (EEG `  N )
) b )  /\  ( y ( dist `  (EEG `  N )
) z )  =  ( b ( dist `  (EEG `  N )
) c ) )  /\  ( ( x ( dist `  (EEG `  N ) ) u )  =  ( a ( dist `  (EEG `  N ) ) v )  /\  ( y ( dist `  (EEG `  N ) ) u )  =  ( b ( dist `  (EEG `  N ) ) v ) ) ) ) )
154146, 153anbi12d 708 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( ( x  =/=  y  /\  y  Btwn  <. x ,  z
>.  /\  b  Btwn  <. a ,  c >. )  /\  ( ( <. x ,  y >.Cgr <. a ,  b >.  /\  <. y ,  z >.Cgr <. b ,  c >. )  /\  ( <. x ,  u >.Cgr
<. a ,  v >.  /\  <. y ,  u >.Cgr
<. b ,  v >.
) ) )  <->  ( (
x  =/=  y  /\  y  e.  ( x
(Itv `  (EEG `  N
) ) z )  /\  b  e.  ( a (Itv `  (EEG `  N ) ) c ) )  /\  (
( ( x (
dist `  (EEG `  N
) ) y )  =  ( a (
dist `  (EEG `  N
) ) b )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( b (
dist `  (EEG `  N
) ) c ) )  /\  ( ( x ( dist `  (EEG `  N ) ) u )  =  ( a ( dist `  (EEG `  N ) ) v )  /\  ( y ( dist `  (EEG `  N ) ) u )  =  ( b ( dist `  (EEG `  N ) ) v ) ) ) ) ) )
155122, 12, 13, 128, 130, 136, 138ecgrtg 24407 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( <. z ,  u >.Cgr
<. c ,  v >.  <->  ( z ( dist `  (EEG `  N ) ) u )  =  ( c ( dist `  (EEG `  N ) ) v ) ) )
156143, 154, 1553imtr3d 267 . . . . . . . . 9  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( z  e.  (
Base `  (EEG `  N
) )  /\  u  e.  ( Base `  (EEG `  N ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  -> 
( ( ( x  =/=  y  /\  y  e.  ( x (Itv `  (EEG `  N ) ) z )  /\  b  e.  ( a (Itv `  (EEG `  N ) ) c ) )  /\  ( ( ( x ( dist `  (EEG `  N ) ) y )  =  ( a ( dist `  (EEG `  N ) ) b )  /\  ( y ( dist `  (EEG `  N ) ) z )  =  ( b ( dist `  (EEG `  N ) ) c ) )  /\  (
( x ( dist `  (EEG `  N )
) u )  =  ( a ( dist `  (EEG `  N )
) v )  /\  ( y ( dist `  (EEG `  N )
) u )  =  ( b ( dist `  (EEG `  N )
) v ) ) ) )  ->  (
z ( dist `  (EEG `  N ) ) u )  =  ( c ( dist `  (EEG `  N ) ) v ) ) )
157156ralrimivvva 2804 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( z  e.  ( Base `  (EEG `  N ) )  /\  u  e.  ( Base `  (EEG `  N )
)  /\  a  e.  ( Base `  (EEG `  N
) ) ) )  ->  A. b  e.  (
Base `  (EEG `  N
) ) A. c  e.  ( Base `  (EEG `  N ) ) A. v  e.  ( Base `  (EEG `  N )
) ( ( ( x  =/=  y  /\  y  e.  ( x
(Itv `  (EEG `  N
) ) z )  /\  b  e.  ( a (Itv `  (EEG `  N ) ) c ) )  /\  (
( ( x (
dist `  (EEG `  N
) ) y )  =  ( a (
dist `  (EEG `  N
) ) b )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( b (
dist `  (EEG `  N
) ) c ) )  /\  ( ( x ( dist `  (EEG `  N ) ) u )  =  ( a ( dist `  (EEG `  N ) ) v )  /\  ( y ( dist `  (EEG `  N ) ) u )  =  ( b ( dist `  (EEG `  N ) ) v ) ) ) )  ->  ( z (
dist `  (EEG `  N
) ) u )  =  ( c (
dist `  (EEG `  N
) ) v ) ) )
158157ralrimivvva 2804 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  A. z  e.  ( Base `  (EEG `  N ) ) A. u  e.  ( Base `  (EEG `  N )
) A. a  e.  ( Base `  (EEG `  N ) ) A. b  e.  ( Base `  (EEG `  N )
) A. c  e.  ( Base `  (EEG `  N ) ) A. v  e.  ( Base `  (EEG `  N )
) ( ( ( x  =/=  y  /\  y  e.  ( x
(Itv `  (EEG `  N
) ) z )  /\  b  e.  ( a (Itv `  (EEG `  N ) ) c ) )  /\  (
( ( x (
dist `  (EEG `  N
) ) y )  =  ( a (
dist `  (EEG `  N
) ) b )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( b (
dist `  (EEG `  N
) ) c ) )  /\  ( ( x ( dist `  (EEG `  N ) ) u )  =  ( a ( dist `  (EEG `  N ) ) v )  /\  ( y ( dist `  (EEG `  N ) ) u )  =  ( b ( dist `  (EEG `  N ) ) v ) ) ) )  ->  ( z (
dist `  (EEG `  N
) ) u )  =  ( c (
dist `  (EEG `  N
) ) v ) ) )
159158ralrimivva 2803 . . . . . 6  |-  ( N  e.  NN  ->  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) A. z  e.  ( Base `  (EEG `  N ) ) A. u  e.  ( Base `  (EEG `  N )
) A. a  e.  ( Base `  (EEG `  N ) ) A. b  e.  ( Base `  (EEG `  N )
) A. c  e.  ( Base `  (EEG `  N ) ) A. v  e.  ( Base `  (EEG `  N )
) ( ( ( x  =/=  y  /\  y  e.  ( x
(Itv `  (EEG `  N
) ) z )  /\  b  e.  ( a (Itv `  (EEG `  N ) ) c ) )  /\  (
( ( x (
dist `  (EEG `  N
) ) y )  =  ( a (
dist `  (EEG `  N
) ) b )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( b (
dist `  (EEG `  N
) ) c ) )  /\  ( ( x ( dist `  (EEG `  N ) ) u )  =  ( a ( dist `  (EEG `  N ) ) v )  /\  ( y ( dist `  (EEG `  N ) ) u )  =  ( b ( dist `  (EEG `  N ) ) v ) ) ) )  ->  ( z (
dist `  (EEG `  N
) ) u )  =  ( c (
dist `  (EEG `  N
) ) v ) ) )
160 simpll 751 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  ->  N  e.  NN )
1617adantr 463 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  ->  x  e.  ( EE `  N ) )
1629adantr 463 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  -> 
y  e.  ( EE
`  N ) )
163 simprl 754 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  -> 
a  e.  ( Base `  (EEG `  N )
) )
164160, 5syl 16 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  -> 
( EE `  N
)  =  ( Base `  (EEG `  N )
) )
165163, 164eleqtrrd 2473 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  -> 
a  e.  ( EE
`  N ) )
166 simprr 755 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  -> 
b  e.  ( Base `  (EEG `  N )
) )
167166, 164eleqtrrd 2473 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  -> 
b  e.  ( EE
`  N ) )
168 axsegcon 24351 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( EE `  N )  /\  y  e.  ( EE `  N ) )  /\  ( a  e.  ( EE `  N )  /\  b  e.  ( EE `  N ) ) )  ->  E. z  e.  ( EE `  N
) ( y  Btwn  <.
x ,  z >.  /\  <. y ,  z
>.Cgr <. a ,  b
>. ) )
169160, 161, 162, 165, 167, 168syl122anc 1235 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  ->  E. z  e.  ( EE `  N ) ( y  Btwn  <. x ,  z >.  /\  <. y ,  z >.Cgr <. a ,  b >. )
)
170 simplll 757 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  N  e.  NN )
1714ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  x  e.  ( Base `  (EEG `  N ) ) )
172 simpr 459 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  z  e.  ( EE `  N
) )
173164adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  ( EE `  N )  =  ( Base `  (EEG `  N ) ) )
174172, 173eleqtrd 2472 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  z  e.  ( Base `  (EEG `  N ) ) )
1758ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  y  e.  ( Base `  (EEG `  N ) ) )
176170, 12, 31, 171, 174, 175ebtwntg 24406 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  (
y  Btwn  <. x ,  z >.  <->  y  e.  ( x (Itv `  (EEG `  N ) ) z ) ) )
177 simplrl 759 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  a  e.  ( Base `  (EEG `  N ) ) )
178 simplrr 760 . . . . . . . . . . . 12  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  b  e.  ( Base `  (EEG `  N ) ) )
179170, 12, 13, 175, 174, 177, 178ecgrtg 24407 . . . . . . . . . . 11  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  ( <. y ,  z >.Cgr <. a ,  b >.  <->  ( y ( dist `  (EEG `  N ) ) z )  =  ( a ( dist `  (EEG `  N ) ) b ) ) )
180176, 179anbi12d 708 . . . . . . . . . 10  |-  ( ( ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N ) )  /\  y  e.  ( Base `  (EEG `  N )
) ) )  /\  ( a  e.  (
Base `  (EEG `  N
) )  /\  b  e.  ( Base `  (EEG `  N ) ) ) )  /\  z  e.  ( EE `  N
) )  ->  (
( y  Btwn  <. x ,  z >.  /\  <. y ,  z >.Cgr <. a ,  b >. )  <->  ( y  e.  ( x (Itv `  (EEG `  N
) ) z )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( a (
dist `  (EEG `  N
) ) b ) ) ) )
181164, 180rexeqbidva 2996 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  -> 
( E. z  e.  ( EE `  N
) ( y  Btwn  <.
x ,  z >.  /\  <. y ,  z
>.Cgr <. a ,  b
>. )  <->  E. z  e.  (
Base `  (EEG `  N
) ) ( y  e.  ( x (Itv
`  (EEG `  N
) ) z )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( a (
dist `  (EEG `  N
) ) b ) ) ) )
182169, 181mpbid 210 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b  e.  ( Base `  (EEG `  N )
) ) )  ->  E. z  e.  ( Base `  (EEG `  N
) ) ( y  e.  ( x (Itv
`  (EEG `  N
) ) z )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( a (
dist `  (EEG `  N
) ) b ) ) )
183182ralrimivva 2803 . . . . . . 7  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  A. a  e.  ( Base `  (EEG `  N ) ) A. b  e.  ( Base `  (EEG `  N )
) E. z  e.  ( Base `  (EEG `  N ) ) ( y  e.  ( x (Itv `  (EEG `  N
) ) z )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( a (
dist `  (EEG `  N
) ) b ) ) )
184183ralrimivva 2803 . . . . . 6  |-  ( N  e.  NN  ->  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) A. a  e.  ( Base `  (EEG `  N ) ) A. b  e.  ( Base `  (EEG `  N )
) E. z  e.  ( Base `  (EEG `  N ) ) ( y  e.  ( x (Itv `  (EEG `  N
) ) z )  /\  ( y (
dist `  (EEG `  N
) ) z )  =  ( a (
dist `  (EEG `  N
) ) b ) ) )
1852, 159, 184jca32 533 . . . . 5  |-  ( N  e.  NN  ->  (
(EEG `  N )  e.  _V  /\  ( A. x  e.  ( Base `  (EEG `  N )
) A. y  e.  ( Base `  (EEG `  N ) ) A. z  e.  ( Base `  (EEG `  N )
) A. u  e.  ( Base `  (EEG `  N ) ) A. a  e.  ( Base `  (EEG `  N )
) A. b  e.  ( Base `  (EEG `  N ) ) A. c  e.  ( Base `  (EEG `  N )
) A. v  e.  ( Base `  (EEG `  N ) ) ( ( ( x  =/=  y  /\  y  e.  ( x (Itv `  (EEG `  N ) ) z )  /\