Metamath Proof Explorer

Theorem eengtrkge

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

Ref Expression
Assertion eengtrkge 
|- ( N e. NN -> ( EEG ` N ) e. TarskiGE )

Proof

Step Hyp Ref Expression
1 fvexd 
 |-  ( N e. NN -> ( EEG ` N ) e. _V )
2 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 )
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 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 ) )
8 simprr 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> y e. ( Base ` ( EEG ` N ) ) )
9 8 5 eleqtrrd 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) ) ) -> y e. ( EE ` N ) )
10 9 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 ) )
11 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 ) ) )
12 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. ( Base ` ( EEG ` N ) ) )
13 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 ) ) )
14 simpr3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> z e. ( Base ` ( EEG ` N ) ) )
15 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 ) ) )
16 14 15 eleqtrrd 
 |-  ( ( N e. NN /\ ( x e. ( Base ` ( EEG ` N ) ) /\ y e. ( Base ` ( EEG ` N ) ) /\ z e. ( Base ` ( EEG ` N ) ) ) ) -> z e. ( EE ` N ) )
17 2 11 12 13 16 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 ) )
18 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 ) ) )
19 4 ad2antrr 
 |-  ( ( ( 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 ) ) )
20 18 19 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 ) )
21 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 ) ) )
22 21 19 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 ) )
23 axeuclid 
 |-  ( ( 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 , v >. /\ u Btwn <. y , z >. /\ x =/= u ) -> E. a e. ( EE ` N ) E. b e. ( EE ` N ) ( y Btwn <. x , a >. /\ z Btwn <. x , b >. /\ v Btwn <. a , b >. ) ) )
24 2 7 10 17 20 22 23 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 , v >. /\ u Btwn <. y , z >. /\ x =/= u ) -> E. a e. ( EE ` N ) E. b e. ( EE ` N ) ( y Btwn <. x , a >. /\ z Btwn <. x , b >. /\ v Btwn <. a , b >. ) ) )
25 eqid 
 |-  ( Base ` ( EEG ` N ) ) = ( Base ` ( EEG ` N ) )
26 eqid 
 |-  ( Itv ` ( EEG ` N ) ) = ( Itv ` ( EEG ` N ) )
27 2 25 26 11 21 18 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 , v >. <-> u e. ( x ( Itv ` ( EEG ` N ) ) v ) ) )
28 2 25 26 12 13 18 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 <. y , z >. <-> u e. ( y ( Itv ` ( EEG ` N ) ) z ) ) )
29 27 28 3anbi12d 
 |-  ( ( ( 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 , v >. /\ u Btwn <. y , z >. /\ x =/= u ) <-> ( u e. ( x ( Itv ` ( EEG ` N ) ) v ) /\ u e. ( y ( Itv ` ( EEG ` N ) ) z ) /\ x =/= u ) ) )
30 19 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 ) ) )
31 2 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) /\ b e. ( EE ` N ) ) -> N e. NN )
32 11 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) /\ b e. ( EE ` N ) ) -> x e. ( Base ` ( EEG ` N ) ) )
33 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 ) )
34 33 30 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 ) ) )
35 34 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 ) ) /\ b e. ( EE ` N ) ) -> a e. ( Base ` ( EEG ` N ) ) )
36 12 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) /\ b e. ( EE ` N ) ) -> y e. ( Base ` ( EEG ` N ) ) )
37 31 25 26 32 35 36 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 ) ) /\ b e. ( EE ` N ) ) -> ( y Btwn <. x , a >. <-> y e. ( x ( Itv ` ( EEG ` N ) ) a ) ) )
38 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 ) ) /\ b e. ( EE ` N ) ) -> b e. ( EE ` N ) )
39 19 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) /\ b e. ( EE ` N ) ) -> ( EE ` N ) = ( Base ` ( EEG ` N ) ) )
40 38 39 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 ) ) /\ b e. ( EE ` N ) ) -> b e. ( Base ` ( EEG ` N ) ) )
41 13 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) /\ b e. ( EE ` N ) ) -> z e. ( Base ` ( EEG ` N ) ) )
42 31 25 26 32 40 41 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 ) ) /\ b e. ( EE ` N ) ) -> ( z Btwn <. x , b >. <-> z e. ( x ( Itv ` ( EEG ` N ) ) b ) ) )
43 21 ad2antrr 
 |-  ( ( ( ( ( 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 ) ) /\ b e. ( EE ` N ) ) -> v e. ( Base ` ( EEG ` N ) ) )
44 31 25 26 35 40 43 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 ) ) /\ b e. ( EE ` N ) ) -> ( v Btwn <. a , b >. <-> v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) )
45 37 42 44 3anbi123d 
 |-  ( ( ( ( ( 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 ) ) /\ b e. ( EE ` N ) ) -> ( ( y Btwn <. x , a >. /\ z Btwn <. x , b >. /\ v Btwn <. a , b >. ) <-> ( y e. ( x ( Itv ` ( EEG ` N ) ) a ) /\ z e. ( x ( Itv ` ( EEG ` N ) ) b ) /\ v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) ) )
46 30 45 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 ) ) ) ) /\ a e. ( EE ` N ) ) -> ( E. b e. ( EE ` N ) ( y Btwn <. x , a >. /\ z Btwn <. x , b >. /\ v Btwn <. a , b >. ) <-> E. b e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) a ) /\ z e. ( x ( Itv ` ( EEG ` N ) ) b ) /\ v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) ) )
47 19 46 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 ) E. b e. ( EE ` N ) ( y Btwn <. x , a >. /\ z Btwn <. x , b >. /\ v Btwn <. a , b >. ) <-> E. a e. ( Base ` ( EEG ` N ) ) E. b e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) a ) /\ z e. ( x ( Itv ` ( EEG ` N ) ) b ) /\ v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) ) )
48 24 29 47 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 ) ) v ) /\ u e. ( y ( Itv ` ( EEG ` N ) ) z ) /\ x =/= u ) -> E. a e. ( Base ` ( EEG ` N ) ) E. b e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) a ) /\ z e. ( x ( Itv ` ( EEG ` N ) ) b ) /\ v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) ) )
49 48 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 ) ) v ) /\ u e. ( y ( Itv ` ( EEG ` N ) ) z ) /\ x =/= u ) -> E. a e. ( Base ` ( EEG ` N ) ) E. b e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) a ) /\ z e. ( x ( Itv ` ( EEG ` N ) ) b ) /\ v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) ) )
50 49 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 ) ) v ) /\ u e. ( y ( Itv ` ( EEG ` N ) ) z ) /\ x =/= u ) -> E. a e. ( Base ` ( EEG ` N ) ) E. b e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) a ) /\ z e. ( x ( Itv ` ( EEG ` N ) ) b ) /\ v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) ) )
51 eqid 
 |-  ( dist ` ( EEG ` N ) ) = ( dist ` ( EEG ` N ) )
52 25 51 26 istrkge 
 |-  ( ( EEG ` N ) e. TarskiGE <-> ( ( 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. v e. ( Base ` ( EEG ` N ) ) ( ( u e. ( x ( Itv ` ( EEG ` N ) ) v ) /\ u e. ( y ( Itv ` ( EEG ` N ) ) z ) /\ x =/= u ) -> E. a e. ( Base ` ( EEG ` N ) ) E. b e. ( Base ` ( EEG ` N ) ) ( y e. ( x ( Itv ` ( EEG ` N ) ) a ) /\ z e. ( x ( Itv ` ( EEG ` N ) ) b ) /\ v e. ( a ( Itv ` ( EEG ` N ) ) b ) ) ) ) )
53 1 50 52 sylanbrc 
 |-  ( N e. NN -> ( EEG ` N ) e. TarskiGE )