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

Theorem eengtrkg 23150
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 5698 . . . . . . 7  |-  (EEG `  N )  e.  _V
21a1i 11 . . . . . 6  |-  ( N  e.  NN  ->  (EEG `  N )  e.  _V )
3 simpl 454 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  N  e.  NN )
4 simprl 750 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  x  e.  ( Base `  (EEG `  N
) ) )
5 eengbas 23146 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  ( EE `  N )  =  ( Base `  (EEG `  N ) ) )
63, 5syl 16 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
74, 6eleqtrrd 2518 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  x  e.  ( EE `  N ) )
8 simprr 751 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  y  e.  ( Base `  (EEG `  N
) ) )
98, 6eleqtrrd 2518 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  y  e.  ( EE `  N ) )
10 axcgrrflx 23079 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  x  e.  ( EE `  N )  /\  y  e.  ( EE `  N
) )  ->  <. x ,  y >.Cgr <. y ,  x >. )
113, 7, 9, 10syl3anc 1213 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  <. x ,  y >.Cgr <. y ,  x >. )
12 eqid 2441 . . . . . . . . . 10  |-  ( Base `  (EEG `  N )
)  =  ( Base `  (EEG `  N )
)
13 eqid 2441 . . . . . . . . . 10  |-  ( dist `  (EEG `  N )
)  =  ( dist `  (EEG `  N )
)
143, 12, 13, 4, 8, 8, 4ecgrtg 23148 . . . . . . . . 9  |-  ( ( 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 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( x
( dist `  (EEG `  N
) ) y )  =  ( y (
dist `  (EEG `  N
) ) x ) )
1615ralrimivva 2806 . . . . . . 7  |-  ( 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 454 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  ->  N  e.  NN )
18 simpr1 989 . . . . . . . . . 10  |-  ( ( 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 990 . . . . . . . . . 10  |-  ( ( 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 991 . . . . . . . . . 10  |-  ( ( 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 23148 . . . . . . . . 9  |-  ( ( 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 1144 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  ->  x  e.  ( EE `  N ) )
2393adantr3 1144 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
y  e.  ( EE
`  N ) )
2417, 5syl 16 . . . . . . . . . . 11  |-  ( ( 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 2518 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  -> 
z  e.  ( EE
`  N ) )
26 axcgrid 23081 . . . . . . . . . 10  |-  ( ( 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 1215 . . . . . . . . 9  |-  ( ( 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 . . . . . . . 8  |-  ( ( 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 2807 . . . . . . 7  |-  ( 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 )
)
3016, 29jca 529 . . . . . 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 )  /\  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 )
) )
312, 30jca 529 . . . . 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 )
) ) )
32 eqid 2441 . . . . . 6  |-  (Itv `  (EEG `  N ) )  =  (Itv `  (EEG `  N ) )
3312, 13, 32istrkgc 22860 . . . . 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 )
) ) )
3431, 33sylibr 212 . . . 4  |-  ( N  e.  NN  ->  (EEG `  N )  e. TarskiGC )
353, 12, 32, 4, 4, 8ebtwntg 23147 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  Btwn  <. x ,  x >.  <-> 
y  e.  ( x (Itv `  (EEG `  N
) ) x ) ) )
36 axbtwnid 23104 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN  /\  y  e.  ( EE `  N )  /\  x  e.  ( EE `  N
) )  ->  (
y  Btwn  <. x ,  x >.  ->  y  =  x ) )
373, 9, 7, 36syl3anc 1213 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  Btwn  <. x ,  x >.  ->  y  =  x ) )
3835, 37sylbird 235 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  e.  ( x (Itv `  (EEG `  N ) ) x )  ->  y  =  x ) )
3938imp 429 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  y  e.  ( x (Itv `  (EEG `  N ) ) x ) )  -> 
y  =  x )
4039eqcomd 2446 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  y  e.  ( x (Itv `  (EEG `  N ) ) x ) )  ->  x  =  y )
4140ex 434 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  ( y  e.  ( x (Itv `  (EEG `  N ) ) x )  ->  x  =  y ) )
4241ralrimivva 2806 . . . . . . 7  |-  ( N  e.  NN  ->  A. x  e.  ( Base `  (EEG `  N ) ) A. y  e.  ( Base `  (EEG `  N )
) ( y  e.  ( x (Itv `  (EEG `  N ) ) x )  ->  x  =  y ) )
433adantr 462 . . . . . . . . . . 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
) ) ) )  ->  N  e.  NN )
447adantr 462 . . . . . . . . . . . 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
) ) ) )  ->  x  e.  ( EE `  N ) )
459adantr 462 . . . . . . . . . . . 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
) ) ) )  ->  y  e.  ( EE `  N ) )
464adantr 462 . . . . . . . . . . . . 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
) ) ) )  ->  x  e.  (
Base `  (EEG `  N
) ) )
478adantr 462 . . . . . . . . . . . . 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
) ) ) )  ->  y  e.  (
Base `  (EEG `  N
) ) )
48 simpr1 989 . . . . . . . . . . . . 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
) ) ) )  ->  z  e.  (
Base `  (EEG `  N
) ) )
4943, 46, 47, 48, 25syl13anc 1215 . . . . . . . . . . . 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
) ) ) )  ->  z  e.  ( EE `  N ) )
5044, 45, 493jca 1163 . . . . . . . . . . 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.  ( EE `  N
)  /\  y  e.  ( EE `  N )  /\  z  e.  ( EE `  N ) ) )
51 simpr2 990 . . . . . . . . . . . . 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
) ) ) )  ->  u  e.  (
Base `  (EEG `  N
) ) )
5243, 5syl 16 . . . . . . . . . . . . 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
) ) ) )  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
5351, 52eleqtrrd 2518 . . . . . . . . . . . 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
) ) ) )  ->  u  e.  ( EE `  N ) )
54 simpr3 991 . . . . . . . . . . . . 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
) ) ) )  ->  v  e.  (
Base `  (EEG `  N
) ) )
5554, 52eleqtrrd 2518 . . . . . . . . . . . 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
) ) ) )  ->  v  e.  ( EE `  N ) )
5653, 55jca 529 . . . . . . . . . . 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.  ( EE `  N
)  /\  v  e.  ( EE `  N ) ) )
57 axpasch 23106 . . . . . . . . . . 11  |-  ( ( 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 >. ) ) )
5843, 50, 56, 57syl3anc 1213 . . . . . . . . . 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
>.  /\  v  Btwn  <. y ,  z >. )  ->  E. a  e.  ( EE `  N ) ( a  Btwn  <. u ,  y >.  /\  a  Btwn  <. v ,  x >. ) ) )
5943, 12, 32, 46, 48, 51ebtwntg 23147 . . . . . . . . . . . 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
) ) ) )  ->  ( u  Btwn  <.
x ,  z >.  <->  u  e.  ( x (Itv
`  (EEG `  N
) ) z ) ) )
6043, 12, 32, 47, 48, 54ebtwntg 23147 . . . . . . . . . . . 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
) ) ) )  ->  ( v  Btwn  <.
y ,  z >.  <->  v  e.  ( y (Itv
`  (EEG `  N
) ) z ) ) )
6159, 60anbi12d 705 . . . . . . . . . . 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 
Btwn  <. x ,  z
>.  /\  v  Btwn  <. y ,  z >. )  <->  ( u  e.  ( x (Itv `  (EEG `  N
) ) z )  /\  v  e.  ( y (Itv `  (EEG `  N ) ) z ) ) ) )
6243adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
6351adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) )
6447adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) )
65 simpr 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
6652adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
) )
6765, 66eleqtrd 2517 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) )
6862, 12, 32, 63, 64, 67ebtwntg 23147 . . . . . . . . . . . . 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  Btwn  <. u ,  y >.  <->  a  e.  ( u (Itv `  (EEG `  N ) ) y ) ) )
6954adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) )
7046adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
) )
7162, 12, 32, 69, 70, 67ebtwntg 23147 . . . . . . . . . . . . 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  Btwn  <. v ,  x >.  <->  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) )
7268, 71anbi12d 705 . . . . . . . . . . . 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  Btwn  <.
u ,  y >.  /\  a  Btwn  <. v ,  x >. )  <->  ( a  e.  ( u (Itv `  (EEG `  N ) ) y )  /\  a  e.  ( v (Itv `  (EEG `  N ) ) x ) ) ) )
7352, 72rexeqbidva 2932 . . . . . . . . . . 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
) ) ) )  ->  ( 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 ) ) ) )
7461, 73imbi12d 320 . . . . . . . . . 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 >.  /\  v  Btwn  <. y ,  z
>. )  ->  E. a  e.  ( EE `  N
) ( a  Btwn  <.
u ,  y >.  /\  a  Btwn  <. v ,  x >. ) )  <->  ( (
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 ) ) ) ) )
7558, 74mpbid 210 . . . . . . . . 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  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 ) ) ) )
7675ralrimivvva 2807 . . . . . . . 8  |-  ( ( 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 ) ) ) )
7776ralrimivva 2806 . . . . . . 7  |-  ( 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 ) ) ) )
78 simpl 454 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  N  e.  NN )
79 elpwi 3866 . . . . . . . . . . . 12  |-  ( s  e.  ~P ( Base `  (EEG `  N )
)  ->  s  C_  ( Base `  (EEG `  N
) ) )
8079ad2antrl 722 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  s  C_  ( Base `  (EEG `  N
) ) )
8178, 5syl 16 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  ( EE `  N )  =  (
Base `  (EEG `  N
) ) )
8280, 81sseqtr4d 3390 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  s  C_  ( EE `  N ) )
83 elpwi 3866 . . . . . . . . . . . 12  |-  ( t  e.  ~P ( Base `  (EEG `  N )
)  ->  t  C_  ( Base `  (EEG `  N
) ) )
8483ad2antll 723 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  t  C_  ( Base `  (EEG `  N
) ) )
8584, 81sseqtr4d 3390 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  t  C_  ( EE `  N ) )
86 simpll 748 . . . . . . . . . . . 12  |-  ( ( ( 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 )
87 simplrl 754 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
88 simplrr 755 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
89 simpr 458 . . . . . . . . . . . . 13  |-  ( ( ( 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 >. )
9087, 88, 893jca 1163 . . . . . . . . . . . 12  |-  ( ( ( 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 )  /\  t  C_  ( EE `  N )  /\  E. a  e.  ( EE `  N ) A. x  e.  s  A. y  e.  t  x  Btwn  <.
a ,  y >.
) )
91 axcont 23141 . . . . . . . . . . . 12  |-  ( ( 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 >. )
9286, 90, 91syl2anc 656 . . . . . . . . . . 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 >. )
9392ex 434 . . . . . . . . . 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 >. )
)
9478, 82, 85, 93syl12anc 1211 . . . . . . . . 9  |-  ( ( 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 >. ) )
9578ad2antrr 720 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
96 simplr 749 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) )
9781ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
9896, 97eleqtrd 2517 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
9984ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
100 simprr 751 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
10199, 100sseldd 3354 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
10280ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
103 simprl 750 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
104102, 103sseldd 3354 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
10595, 12, 32, 98, 101, 104ebtwntg 23147 . . . . . . . . . . . 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  Btwn  <. a ,  y
>. 
<->  x  e.  ( a (Itv `  (EEG `  N
) ) y ) ) )
1061052ralbidva 2753 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
10781, 106rexeqbidva 2932 . . . . . . . . . 10  |-  ( ( 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 ) ) )
10878ad2antrr 720 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
10980ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
110 simprl 750 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
111109, 110sseldd 3354 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
11284ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
113 simprr 751 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
114112, 113sseldd 3354 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
115 simplr 749 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) )
11681ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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
) ) )
117115, 116eleqtrd 2517 . . . . . . . . . . . . 13  |-  ( ( ( ( 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
) ) )
118108, 12, 32, 111, 114, 117ebtwntg 23147 . . . . . . . . . . . 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  Btwn  <. x ,  y
>. 
<->  b  e.  ( x (Itv `  (EEG `  N
) ) y ) ) )
1191182ralbidva 2753 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
12081, 119rexeqbidva 2932 . . . . . . . . . 10  |-  ( ( 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 ) ) )
121107, 120imbi12d 320 . . . . . . . . 9  |-  ( ( 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 >. )  <->  ( 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 ) ) ) )
12294, 121mpbid 210 . . . . . . . 8  |-  ( ( 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 ) ) )
123122ralrimivva 2806 . . . . . . 7  |-  ( 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 ) ) )
12442, 77, 1233jca 1163 . . . . . 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 )  /\  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 ) ) ) )
1252, 124jca 529 . . . . 5  |-  ( N  e.  NN  ->  (
(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 ) ) ) ) )
12612, 13, 32istrkgb 22861 . . . . 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 ) ) ) ) )
127125, 126sylibr 212 . . . 4  |-  ( N  e.  NN  ->  (EEG `  N )  e. TarskiGB )
12834, 127elind 3537 . . 3  |-  ( N  e.  NN  ->  (EEG `  N )  e.  (TarskiGC  i^i TarskiGB ) )
129 simplll 752 . . . . . . . . . . . 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 )
) ) )  ->  N  e.  NN )
1304ad2antrr 720 . . . . . . . . . . . . 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  e.  ( Base `  (EEG `  N )
) )
131129, 5syl 16 . . . . . . . . . . . . 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 )
) ) )  -> 
( EE `  N
)  =  ( Base `  (EEG `  N )
) )
132130, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE `  N ) )
1338ad2antrr 720 . . . . . . . . . . . . 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  e.  ( Base `  (EEG `  N )
) )
134133, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE
`  N ) )
135129, 132, 1343jca 1163 . . . . . . . . . . 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  /\  x  e.  ( EE
`  N )  /\  y  e.  ( EE `  N ) ) )
136 simplr1 1025 . . . . . . . . . . . . 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 )
) ) )  -> 
z  e.  ( Base `  (EEG `  N )
) )
137136, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE
`  N ) )
138 simplr2 1026 . . . . . . . . . . . . 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 )
) ) )  ->  u  e.  ( Base `  (EEG `  N )
) )
139138, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE `  N ) )
140 simplr3 1027 . . . . . . . . . . . . 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 )
) ) )  -> 
a  e.  ( Base `  (EEG `  N )
) )
141140, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE
`  N ) )
142137, 139, 1413jca 1163 . . . . . . . . . . 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 )  /\  u  e.  ( EE `  N )  /\  a  e.  ( EE `  N ) ) )
143 simpr1 989 . . . . . . . . . . . . 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 )
) ) )  -> 
b  e.  ( Base `  (EEG `  N )
) )
144143, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE
`  N ) )
145 simpr2 990 . . . . . . . . . . . . 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 )
) ) )  -> 
c  e.  ( Base `  (EEG `  N )
) )
146145, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE
`  N ) )
147 simpr3 991 . . . . . . . . . . . . 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 )
) ) )  -> 
v  e.  ( Base `  (EEG `  N )
) )
148147, 131eleqtrrd 2518 . . . . . . . . . . . 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.  ( EE
`  N ) )
149144, 146, 1483jca 1163 . . . . . . . . . . 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 )  /\  c  e.  ( EE `  N )  /\  v  e.  ( EE `  N ) ) )
150 ax5seg 23103 . . . . . . . . . . . 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
>. ) )
151 3anass 964 . . . . . . . . . . . . 13  |-  ( ( ( 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 >.
) ) ) )
152151imbi1i 325 . . . . . . . . . . . 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 >.
) )  ->  <. z ,  u >.Cgr <. c ,  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 >.
) ) )  ->  <. z ,  u >.Cgr <.
c ,  v >.
) )
153150, 152sylib 196 . . . . . . . . . . 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 >.
) )
154135, 142, 149, 153syl3anc 1213 . . . . . . . . . 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 >.
) )
155 biidd 237 . . . . . . . . . . . . 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  <->  x  =/=  y ) )
1563ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
157156, 12, 32, 130, 136, 133ebtwntg 23147 . . . . . . . . . . . . 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  Btwn  <. x ,  z >.  <->  y  e.  ( x (Itv `  (EEG `  N ) ) z ) ) )
158156, 12, 32, 140, 145, 143ebtwntg 23147 . . . . . . . . . . . . 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 )
) ) )  -> 
( b  Btwn  <. a ,  c >.  <->  b  e.  ( a (Itv `  (EEG `  N ) ) c ) ) )
159155, 157, 1583anbi123d 1284 . . . . . . . . . . . 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  /\  y  Btwn  <.
x ,  z >.  /\  b  Btwn  <. a ,  c >. )  <->  ( x  =/=  y  /\  y  e.  ( x
(Itv `  (EEG `  N
) ) z )  /\  b  e.  ( a (Itv `  (EEG `  N ) ) c ) ) ) )
160156, 12, 13, 130, 133, 140, 143ecgrtg 23148 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )
161156, 12, 13, 133, 136, 143, 145ecgrtg 23148 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )
162160, 161anbi12d 705 . . . . . . . . . . . . 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 >.  /\  <. 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 ) ) ) )
163156, 12, 13, 130, 138, 140, 147ecgrtg 23148 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )
164156, 12, 13, 133, 138, 143, 147ecgrtg 23148 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) ) )
165163, 164anbi12d 705 . . . . . . . . . . . . 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
>.  /\  <. 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 ) ) ) )
166162, 165anbi12d 705 . . . . . . . . . . . 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 ,  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 ) ) ) ) )
167159, 166anbi12d 705 . . . . . . . . . . 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 >.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 ) ) ) ) ) )
168156, 12, 13, 136, 138, 145, 147ecgrtg 23148 . . . . . . . . . . 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 ,  u >.Cgr
<. c ,  v >.  <->  ( z ( dist `  (EEG `  N ) ) u )  =  ( c ( dist `  (EEG `  N ) ) v ) ) )
169167, 168imbi12d 320 . . . . . . . . . 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 >.
)  <->  ( ( ( 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 ) ) ) )
170154, 169mpbid 210 . . . . . . . . 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 ) ) )
171170ralrimivvva 2807 . . . . . . . 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 ) ) )
172171ralrimivvva 2807 . . . . . . 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 ) ) )
173172ralrimivva 2806 . . . . . 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 ) ) )
1743adantr 462 . . . . . . . . . 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 )
1757adantr 462 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b