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

Theorem eengtrkg 23243
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 5713 . . . . . . 7  |-  (EEG `  N )  e.  _V
21a1i 11 . . . . . 6  |-  ( N  e.  NN  ->  (EEG `  N )  e.  _V )
3 simpl 457 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  N  e.  NN )
4 simprl 755 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  x  e.  ( Base `  (EEG `  N
) ) )
5 eengbas 23239 . . . . . . . . . . . 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 2520 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  x  e.  ( EE `  N ) )
8 simprr 756 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  y  e.  ( Base `  (EEG `  N
) ) )
98, 6eleqtrrd 2520 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  y  e.  ( EE `  N ) )
10 axcgrrflx 23172 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  x  e.  ( EE `  N )  /\  y  e.  ( EE `  N
) )  ->  <. x ,  y >.Cgr <. y ,  x >. )
113, 7, 9, 10syl3anc 1218 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  ->  <. x ,  y >.Cgr <. y ,  x >. )
12 eqid 2443 . . . . . . . . . 10  |-  ( Base `  (EEG `  N )
)  =  ( Base `  (EEG `  N )
)
13 eqid 2443 . . . . . . . . . 10  |-  ( dist `  (EEG `  N )
)  =  ( dist `  (EEG `  N )
)
143, 12, 13, 4, 8, 8, 4ecgrtg 23241 . . . . . . . . 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 2820 . . . . . . 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 457 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  ->  N  e.  NN )
18 simpr1 994 . . . . . . . . . 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 995 . . . . . . . . . 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 996 . . . . . . . . . 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 23241 . . . . . . . . 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 1149 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( x  e.  ( Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) )  /\  z  e.  ( Base `  (EEG `  N )
) ) )  ->  x  e.  ( EE `  N ) )
2393adantr3 1149 . . . . . . . . . 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 2520 . . . . . . . . . 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 23174 . . . . . . . . . 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 1220 . . . . . . . . 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 2821 . . . . . . 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 532 . . . . . 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 532 . . . . 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 2443 . . . . . 6  |-  (Itv `  (EEG `  N ) )  =  (Itv `  (EEG `  N ) )
3312, 13, 32istrkgc 22929 . . . . 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 23240 . . . . . . . . . . . 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 23197 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN  /\  y  e.  ( EE `  N )  /\  x  e.  ( EE `  N
) )  ->  (
y  Btwn  <. x ,  x >.  ->  y  =  x ) )
373, 9, 7, 36syl3anc 1218 . . . . . . . . . . . 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 2448 . . . . . . . . 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 2820 . . . . . . 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 465 . . . . . . . . . . 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 465 . . . . . . . . . . . 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 465 . . . . . . . . . . . 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 465 . . . . . . . . . . . . 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 465 . . . . . . . . . . . . 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 994 . . . . . . . . . . . . 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 1220 . . . . . . . . . . . 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 1168 . . . . . . . . . . 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 995 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 996 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 532 . . . . . . . . . . 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 23199 . . . . . . . . . . 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 1218 . . . . . . . . . 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 23240 . . . . . . . . . . . 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 23240 . . . . . . . . . . . 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 710 . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . 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 2519 . . . . . . . . . . . . . 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 23240 . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . 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 23240 . . . . . . . . . . . . 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 710 . . . . . . . . . . . 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 2946 . . . . . . . . . . 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 2821 . . . . . . . 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 2820 . . . . . . 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 457 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  N  e.  NN )
79 elpwi 3881 . . . . . . . . . . . 12  |-  ( s  e.  ~P ( Base `  (EEG `  N )
)  ->  s  C_  ( Base `  (EEG `  N
) ) )
8079ad2antrl 727 . . . . . . . . . . 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 3405 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  s  C_  ( EE `  N ) )
83 elpwi 3881 . . . . . . . . . . . 12  |-  ( t  e.  ~P ( Base `  (EEG `  N )
)  ->  t  C_  ( Base `  (EEG `  N
) ) )
8483ad2antll 728 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  t  C_  ( Base `  (EEG `  N
) ) )
8584, 81sseqtr4d 3405 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( s  e.  ~P ( Base `  (EEG `  N
) )  /\  t  e.  ~P ( Base `  (EEG `  N ) ) ) )  ->  t  C_  ( EE `  N ) )
86 simpll 753 . . . . . . . . . . . 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 759 . . . . . . . . . . . . 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 760 . . . . . . . . . . . . 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 461 . . . . . . . . . . . . 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 1168 . . . . . . . . . . . 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 23234 . . . . . . . . . . . 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 661 . . . . . . . . . . 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 1216 . . . . . . . . 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 725 . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 2519 . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . 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 3369 . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 755 . . . . . . . . . . . . . 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 3369 . . . . . . . . . . . . 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 23240 . . . . . . . . . . . 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 2767 . . . . . . . . . . 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 2946 . . . . . . . . . 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 725 . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 755 . . . . . . . . . . . . . 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 3369 . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 756 . . . . . . . . . . . . . 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 3369 . . . . . . . . . . . . 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 754 . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 2519 . . . . . . . . . . . . 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 23240 . . . . . . . . . . . 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 2767 . . . . . . . . . . 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 2946 . . . . . . . . . 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 2820 . . . . . . 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 1168 . . . . . 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 532 . . . . 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 22930 . . . . 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 3552 . . 3  |-  ( N  e.  NN  ->  (EEG `  N )  e.  (TarskiGC  i^i TarskiGB ) )
129 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 ) )  /\  a  e.  ( Base `  (EEG `  N )
) ) )  /\  ( b  e.  (
Base `  (EEG `  N
) )  /\  c  e.  ( Base `  (EEG `  N ) )  /\  v  e.  ( Base `  (EEG `  N )
) ) )  ->  N  e.  NN )
1304ad2antrr 725 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 725 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 1168 . . . . . . . . . . 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 1030 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 1031 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 1032 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 1168 . . . . . . . . . . 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 994 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 995 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 996 . . . . . . . . . . . . 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 2520 . . . . . . . . . . . 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 1168 . . . . . . . . . . 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 23196 . . . . . . . . . . . 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 969 . . . . . . . . . . . . 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 1218 . . . . . . . . . 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 725 . . . . . . . . . . . . . 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 23240 . . . . . . . . . . . . 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 23240 . . . . . . . . . . . . 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 1289 . . . . . . . . . . . 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 23241 . . . . . . . . . . . . . 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 23241 . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . 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 23241 . . . . . . . . . . . . . 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 23241 . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . 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 710 . . . . . . . . . . . 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 710 . . . . . . . . . . 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 23241 . . . . . . . . . . 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 2821 . . . . . . . 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 2821 . . . . . . 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 2820 . . . . . 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 465 . . . . . . . . . 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 465 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  ( x  e.  (
Base `  (EEG `  N
) )  /\  y  e.  ( Base `  (EEG `  N ) ) ) )  /\  ( a  e.  ( Base `  (EEG `  N ) )  /\  b