Metamath Proof Explorer

Theorem eengtrkg

Description: The geometry structure for EE ^ N is a Tarski geometry. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Assertion eengtrkg 
|- ( N e. NN -> ( EEG ` N ) e. TarskiG )

Proof

Step Hyp Ref Expression
1 fvexd 
 |-  ( N e. NN -> ( EEG ` N ) e. _V )
2 simpl 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> N e. NN )
3 simprl 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> x e. ( Base ` ( EEG ` N ) ) )
4 eengbas 
 |-  ( N e. NN -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
5 4 adantr 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
6 3 5 eleqtrrd 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> x e. ( EE ` N ) )
7 simprr 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> y e. ( Base ` ( EEG ` N ) ) )
8 7 5 eleqtrrd 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> y e. ( EE ` N ) )
9 axcgrrflx 
 |-  ( ( N e. NN /\ x e. ( EE ` N ) /\ y e. ( EE ` N ) ) -> <. x , y >. Cgr <. y , x >. )
10 2 6 8 9 syl3anc 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> <. x , y >. Cgr <. y , x >. )
11 eqid 
 |-  ( Base ` ( EEG ` N ) ) = ( Base ` ( EEG ` N ) )
12 eqid 
 |-  ( dist ` ( EEG ` N ) ) = ( dist ` ( EEG ` N ) )
13 2 11 12 3 7 7 3 ecgrtg 
 |-  ( ( 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 ) ) )
14 10 13 mpbid 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> ( x ( dist ` ( EEG ` N ) ) y ) = ( y ( dist ` ( EEG ` N ) ) x ) )
15 14 ralrimivva 
 |-  ( 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 ) )
16 simpl 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> N e. NN )
17 simpr1 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> x e. ( Base ` ( EEG ` N ) ) )
18 simpr2 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> y e. ( Base ` ( EEG ` N ) ) )
19 simpr3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> z e. ( Base ` ( EEG ` N ) ) )
20 16 11 12 17 18 19 19 ecgrtg 
 |-  ( ( 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 ) ) )
21 6 3adantr3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> x e. ( EE ` N ) )
22 8 3adantr3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> y e. ( EE ` N ) )
23 4 adantr 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
24 19 23 eleqtrrd 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> z e. ( EE ` N ) )
25 axcgrid 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> ( <. x , y >. Cgr <. z , z >. -> x = y ) )
26 16 21 22 24 25 syl13anc 
 |-  ( ( 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 ) )
27 20 26 sylbird 
 |-  ( ( 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 ) )
28 27 ralrimivvva 
 |-  ( 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 ) )
29 1 15 28 jca32 
 |-  ( 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 ) ) ) )
30 eqid 
 |-  ( Itv ` ( EEG ` N ) ) = ( Itv ` ( EEG ` N ) )
31 11 12 30 istrkgc 
 |-  ( ( 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 ) ) ) )
32 29 31 sylibr 
 |-  ( N e. NN -> ( EEG ` N ) e. TarskiGC )
33 2 11 30 3 3 7 ebtwntg 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> ( y Btwn <. x , x >. <-> y e. ( x ( Itv ` ( EEG ` N ) ) x ) ) )
34 axbtwnid 
 |-  ( ( N e. NN /\ y e. ( EE ` N ) /\ x e. ( EE ` N ) ) -> ( y Btwn <. x , x >. -> y = x ) )
35 2 8 6 34 syl3anc 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> ( y Btwn <. x , x >. -> y = x ) )
36 33 35 sylbird 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> ( y e. ( x ( Itv ` ( EEG ` N ) ) x ) -> y = x ) )
37 36 imp 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ y e. ( x ( Itv ` ( EEG ` N ) ) x ) ) -> y = x )
38 37 equcomd 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ y e. ( x ( Itv ` ( EEG ` N ) ) x ) ) -> x = y )
39 38 ex 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> ( y e. ( x ( Itv ` ( EEG ` N ) ) x ) -> x = y ) )
40 39 ralrimivva 
 |-  ( N e. NN -> A. x e. ( Base ` ( EEG ` N ) ) A. y e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) x ) -> x = y ) )
41 simpll 
 |-  ( ( ( 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 )
42 6 adantr 
 |-  ( ( ( 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 ) )
43 8 adantr 
 |-  ( ( ( 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 ) )
44 3 adantr 
 |-  ( ( ( 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 ) ) )
45 7 adantr 
 |-  ( ( ( 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 ) ) )
46 simpr1 
 |-  ( ( ( 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 ) ) )
47 41 44 45 46 24 syl13anc 
 |-  ( ( ( 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 ) )
48 simpr2 
 |-  ( ( ( 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 ) ) )
49 41 4 syl 
 |-  ( ( ( 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 ) ) )
50 48 49 eleqtrrd 
 |-  ( ( ( 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 ) )
51 simpr3 
 |-  ( ( ( 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 ) ) )
52 51 49 eleqtrrd 
 |-  ( ( ( 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 ) )
53 axpasch 
 |-  ( ( 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 >. ) ) )
54 41 42 43 47 50 52 53 syl132anc 
 |-  ( ( ( 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 >. ) ) )
55 41 11 30 44 46 48 ebtwntg 
 |-  ( ( ( 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 ) ) )
56 41 11 30 45 46 51 ebtwntg 
 |-  ( ( ( 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 ) ) )
57 55 56 anbi12d 
 |-  ( ( ( 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 ) ) ) )
58 simplll 
 |-  ( ( ( ( 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 )
59 48 adantr 
 |-  ( ( ( ( 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 ) ) )
60 45 adantr 
 |-  ( ( ( ( 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 ) ) )
61 simpr 
 |-  ( ( ( ( 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 ) )
62 49 adantr 
 |-  ( ( ( ( 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 ) ) )
63 61 62 eleqtrd 
 |-  ( ( ( ( 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 ) ) )
64 58 11 30 59 60 63 ebtwntg 
 |-  ( ( ( ( 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 ) ) )
65 51 adantr 
 |-  ( ( ( ( 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 ) ) )
66 44 adantr 
 |-  ( ( ( ( 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 ) ) )
67 58 11 30 65 66 63 ebtwntg 
 |-  ( ( ( ( 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 ) ) )
68 64 67 anbi12d 
 |-  ( ( ( ( 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 ) ) ) )
69 49 68 rexeqbidva 
 |-  ( ( ( 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 ) ) ) )
70 54 57 69 3imtr3d 
 |-  ( ( ( 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 ) ) ) )
71 70 ralrimivvva 
 |-  ( ( 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 ) ) ) )
72 71 ralrimivva 
 |-  ( 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 ) ) ) )
73 simpl 
 |-  ( ( N e. NN /\ ( s e. ~P ( Base ` ( EEG ` N ) ) /\ t e. ~P ( Base ` ( EEG ` N ) ) ) ) -> N e. NN )
74 elpwi 
 |-  ( s e. ~P ( Base ` ( EEG ` N ) ) -> s C_ ( Base ` ( EEG ` N ) ) )
75 74 ad2antrl 
 |-  ( ( N e. NN /\ ( s e. ~P ( Base ` ( EEG ` N ) ) /\ t e. ~P ( Base ` ( EEG ` N ) ) ) ) -> s C_ ( Base ` ( EEG ` N ) ) )
76 4 adantr 
 |-  ( ( N e. NN /\ ( s e. ~P ( Base ` ( EEG ` N ) ) /\ t e. ~P ( Base ` ( EEG ` N ) ) ) ) -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
77 75 76 sseqtrrd 
 |-  ( ( N e. NN /\ ( s e. ~P ( Base ` ( EEG ` N ) ) /\ t e. ~P ( Base ` ( EEG ` N ) ) ) ) -> s C_ ( EE ` N ) )
78 elpwi 
 |-  ( t e. ~P ( Base ` ( EEG ` N ) ) -> t C_ ( Base ` ( EEG ` N ) ) )
79 78 ad2antll 
 |-  ( ( N e. NN /\ ( s e. ~P ( Base ` ( EEG ` N ) ) /\ t e. ~P ( Base ` ( EEG ` N ) ) ) ) -> t C_ ( Base ` ( EEG ` N ) ) )
80 79 76 sseqtrrd 
 |-  ( ( N e. NN /\ ( s e. ~P ( Base ` ( EEG ` N ) ) /\ t e. ~P ( Base ` ( EEG ` N ) ) ) ) -> t C_ ( EE ` N ) )
81 simpll 
 |-  ( ( ( 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 )
82 simplrl 
 |-  ( ( ( 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 ) )
83 simplrr 
 |-  ( ( ( 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 ) )
84 simpr 
 |-  ( ( ( 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 >. )
85 axcont 
 |-  ( ( 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 >. )
86 81 82 83 84 85 syl13anc 
 |-  ( ( ( 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 >. )
87 86 ex 
 |-  ( ( 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 >. ) )
88 73 77 80 87 syl12anc 
 |-  ( ( 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 >. ) )
89 simplll 
 |-  ( ( ( ( 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 )
90 simplr 
 |-  ( ( ( ( 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 ) )
91 76 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
92 90 91 eleqtrd 
 |-  ( ( ( ( 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 ) ) )
93 79 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
94 simprr 
 |-  ( ( ( ( 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 )
95 93 94 sseldd 
 |-  ( ( ( ( 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 ) ) )
96 75 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
97 simprl 
 |-  ( ( ( ( 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 )
98 96 97 sseldd 
 |-  ( ( ( ( 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 ) ) )
99 89 11 30 92 95 98 ebtwntg 
 |-  ( ( ( ( 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 ) ) )
100 99 2ralbidva 
 |-  ( ( ( 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 ) ) )
101 76 100 rexeqbidva 
 |-  ( ( 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 ) ) )
102 simplll 
 |-  ( ( ( ( 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 )
103 75 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
104 simprl 
 |-  ( ( ( ( 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 )
105 103 104 sseldd 
 |-  ( ( ( ( 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 ) ) )
106 79 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
107 simprr 
 |-  ( ( ( ( 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 )
108 106 107 sseldd 
 |-  ( ( ( ( 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 ) ) )
109 simplr 
 |-  ( ( ( ( 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 ) )
110 76 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
111 109 110 eleqtrd 
 |-  ( ( ( ( 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 ) ) )
112 102 11 30 105 108 111 ebtwntg 
 |-  ( ( ( ( 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 ) ) )
113 112 2ralbidva 
 |-  ( ( ( 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 ) ) )
114 76 113 rexeqbidva 
 |-  ( ( 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 ) ) )
115 88 101 114 3imtr3d 
 |-  ( ( 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 ) ) )
116 115 ralrimivva 
 |-  ( 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 ) ) )
117 40 72 116 3jca 
 |-  ( 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 ) ) ) )
118 11 12 30 istrkgb 
 |-  ( ( 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 ) ) ) ) )
119 1 117 118 sylanbrc 
 |-  ( N e. NN -> ( EEG ` N ) e. TarskiGB )
120 32 119 elind 
 |-  ( N e. NN -> ( EEG ` N ) e. ( TarskiGC i^i TarskiGB ) )
121 simplll 
 |-  ( ( ( ( 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 )
122 3 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
123 121 4 syl 
 |-  ( ( ( ( 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 ) ) )
124 122 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
125 7 ad2antrr 
 |-  ( ( ( ( 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 ) ) )
126 125 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
127 simplr1 
 |-  ( ( ( ( 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 ) ) )
128 127 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
129 simplr2 
 |-  ( ( ( ( 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 ) ) )
130 129 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
131 simplr3 
 |-  ( ( ( ( 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 ) ) )
132 131 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
133 simpr1 
 |-  ( ( ( ( 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 ) ) )
134 133 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
135 simpr2 
 |-  ( ( ( ( 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 ) ) )
136 135 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
137 simpr3 
 |-  ( ( ( ( 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 ) ) )
138 137 123 eleqtrrd 
 |-  ( ( ( ( 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 ) )
139 3anass 
 |-  ( ( ( 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 >. ) ) ) )
140 ax5seg 
 |-  ( ( ( 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 >. ) )
141 139 140 syl5bir 
 |-  ( ( ( 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 >. ) )
142 121 124 126 128 130 132 134 136 138 141 syl333anc 
 |-  ( ( ( ( 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 >. ) )
143 121 11 30 122 127 125 ebtwntg 
 |-  ( ( ( ( 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 ) ) )
144 121 11 30 131 135 133 ebtwntg 
 |-  ( ( ( ( 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 ) ) )
145 143 144 3anbi23d 
 |-  ( ( ( ( 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 ) ) ) )
146 121 11 12 122 125 131 133 ecgrtg 
 |-  ( ( ( ( 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 ) ) )
147 121 11 12 125 127 133 135 ecgrtg 
 |-  ( ( ( ( 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 ) ) )
148 146 147 anbi12d 
 |-  ( ( ( ( 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 ) ) ) )
149 121 11 12 122 129 131 137 ecgrtg 
 |-  ( ( ( ( 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 ) ) )
150 121 11 12 125 129 133 137 ecgrtg 
 |-  ( ( ( ( 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 ) ) )
151 149 150 anbi12d 
 |-  ( ( ( ( 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 ) ) ) )
152 148 151 anbi12d 
 |-  ( ( ( ( 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 ) ) ) ) )
153 145 152 anbi12d 
 |-  ( ( ( ( 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 ) ) ) ) ) )
154 121 11 12 127 129 135 137 ecgrtg 
 |-  ( ( ( ( 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 ) ) )
155 142 153 154 3imtr3d 
 |-  ( ( ( ( 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 ) ) )
156 155 ralrimivvva 
 |-  ( ( ( 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 ) ) )
157 156 ralrimivvva 
 |-  ( ( 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 ) ) )
158 157 ralrimivva 
 |-  ( 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 ) ) )
159 simpll 
 |-  ( ( ( 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 )
160 6 adantr 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> x e. ( EE ` N ) )
161 8 adantr 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> y e. ( EE ` N ) )
162 simprl 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> a e. ( Base ` ( EEG ` N ) ) )
163 159 4 syl 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
164 162 163 eleqtrrd 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> a e. ( EE ` N ) )
165 simprr 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> b e. ( Base ` ( EEG ` N ) ) )
166 165 163 eleqtrrd 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> b e. ( EE ` N ) )
167 axsegcon 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) /\ ( a e. ( EE ` N ) /\ b e. ( EE ` N ) ) ) -> E. z e. ( EE ` N ) ( y Btwn <. x , z >. /\ <. y , z >. Cgr <. a , b >. ) )
168 159 160 161 164 166 167 syl122anc 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> E. z e. ( EE ` N ) ( y Btwn <. x , z >. /\ <. y , z >. Cgr <. a , b >. ) )
169 simplll 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> N e. NN )
170 3 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> x e. ( Base ` ( EEG ` N ) ) )
171 simpr 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> z e. ( EE ` N ) )
172 163 adantr 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
173 171 172 eleqtrd 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> z e. ( Base ` ( EEG ` N ) ) )
174 7 ad2antrr 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> y e. ( Base ` ( EEG ` N ) ) )
175 169 11 30 170 173 174 ebtwntg 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> ( y Btwn <. x , z >. <-> y e. ( x ( Itv ` ( EEG ` N ) ) z ) ) )
176 simplrl 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> a e. ( Base ` ( EEG ` N ) ) )
177 simplrr 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> b e. ( Base ` ( EEG ` N ) ) )
178 169 11 12 174 173 176 177 ecgrtg 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> ( <. y , z >. Cgr <. a , b >. <-> ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) )
179 175 178 anbi12d 
 |-  ( ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) /\ z e. ( EE ` N ) ) -> ( ( y Btwn <. x , z >. /\ <. y , z >. Cgr <. a , b >. ) <-> ( y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) ) )
180 163 179 rexeqbidva 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> ( E. z e. ( EE ` N ) ( y Btwn <. x , z >. /\ <. y , z >. Cgr <. a , b >. ) <-> E. z e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) ) )
181 168 180 mpbid 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) /\ ( a e. ( Base ` ( EEG ` N ) ) /\ b e. ( Base ` ( EEG ` N ) ) ) ) -> E. z e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) )
182 181 ralrimivva 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> A. a e. ( Base ` ( EEG ` N ) ) A. b e. ( Base ` ( EEG ` N ) ) E. z e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) )
183 182 ralrimivva 
 |-  ( N e. NN -> A. x e. ( Base ` ( EEG ` N ) ) A. y e. ( Base ` ( EEG ` N ) ) A. a e. ( Base ` ( EEG ` N ) ) A. b e. ( Base ` ( EEG ` N ) ) E. z e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) )
184 1 158 183 jca32 
 |-  ( N e. NN -> ( ( EEG ` N ) e. _V /\ ( A. x e. ( Base ` ( EEG ` N ) ) A. y e. ( Base ` ( EEG ` N ) ) A. z e. ( Base ` ( EEG ` N ) ) A. u e. ( Base ` ( EEG ` N ) ) A. a e. ( Base ` ( EEG ` N ) ) A. b e. ( Base ` ( EEG ` N ) ) A. c e. ( Base ` ( EEG ` N ) ) A. v e. ( Base ` ( EEG ` N ) ) ( ( ( x =/= y /\ y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ 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 ) ) /\ A. x e. ( Base ` ( EEG ` N ) ) A. y e. ( Base ` ( EEG ` N ) ) A. a e. ( Base ` ( EEG ` N ) ) A. b e. ( Base ` ( EEG ` N ) ) E. z e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) ) ) )
185 11 12 30 istrkgcb 
 |-  ( ( EEG ` N ) e. TarskiGCB <-> ( ( EEG ` N ) e. _V /\ ( A. x e. ( Base ` ( EEG ` N ) ) A. y e. ( Base ` ( EEG ` N ) ) A. z e. ( Base ` ( EEG ` N ) ) A. u e. ( Base ` ( EEG ` N ) ) A. a e. ( Base ` ( EEG ` N ) ) A. b e. ( Base ` ( EEG ` N ) ) A. c e. ( Base ` ( EEG ` N ) ) A. v e. ( Base ` ( EEG ` N ) ) ( ( ( x =/= y /\ y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ 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 ) ) /\ A. x e. ( Base ` ( EEG ` N ) ) A. y e. ( Base ` ( EEG ` N ) ) A. a e. ( Base ` ( EEG ` N ) ) A. b e. ( Base ` ( EEG ` N ) ) E. z e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) z ) /\ ( y ( dist ` ( EEG ` N ) ) z ) = ( a ( dist ` ( EEG ` N ) ) b ) ) ) ) )
186 184 185 sylibr 
 |-  ( N e. NN -> ( EEG ` N ) e. TarskiGCB )
187 11 30 elntg 
 |-  ( N e. NN -> ( LineG ` ( EEG ` N ) ) = ( x e. ( Base ` ( EEG ` N ) ) , y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) |-> { z e. ( Base ` ( EEG ` N ) ) | ( z e. ( x ( Itv ` ( EEG ` N ) ) y ) \/ x e. ( z ( Itv ` ( EEG ` N ) ) y ) \/ y e. ( x ( Itv ` ( EEG ` N ) ) z ) ) } ) )
188 11 12 30 istrkgl 
 |-  ( ( EEG ` N ) e. { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } <-> ( ( EEG ` N ) e. _V /\ ( LineG ` ( EEG ` N ) ) = ( x e. ( Base ` ( EEG ` N ) ) , y e. ( ( Base ` ( EEG ` N ) ) \ { x } ) |-> { z e. ( Base ` ( EEG ` N ) ) | ( z e. ( x ( Itv ` ( EEG ` N ) ) y ) \/ x e. ( z ( Itv ` ( EEG ` N ) ) y ) \/ y e. ( x ( Itv ` ( EEG ` N ) ) z ) ) } ) ) )
189 1 187 188 sylanbrc 
 |-  ( N e. NN -> ( EEG ` N ) e. { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } )
190 186 189 elind 
 |-  ( N e. NN -> ( EEG ` N ) e. ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
191 120 190 elind 
 |-  ( N e. NN -> ( EEG ` N ) e. ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) )
192 df-trkg 
 |-  TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
193 191 192 eleqtrrdi 
 |-  ( N e. NN -> ( EEG ` N ) e. TarskiG )