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 ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) ∈ TarskiGE )

Proof

Step Hyp Ref Expression
1 fvexd ⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) ∈ V )
2 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑁 ∈ ℕ )
3 simprl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
4 eengbas ⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
5 4 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
6 3 5 eleqtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simprr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
9 8 5 eleqtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
11 3 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
12 8 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
13 simpr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
14 simpr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
15 4 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
16 14 15 eleqtrrd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) )
17 2 11 12 13 16 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) )
18 simpr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
19 4 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
20 18 19 eleqtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) )
21 simpr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
22 21 19 eleqtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) )
23 axeuclid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑢 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑣 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑢 Btwn ⟨ 𝑥 , 𝑣 ⟩ ∧ 𝑢 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑥 , 𝑎 ⟩ ∧ 𝑧 Btwn ⟨ 𝑥 , 𝑏 ⟩ ∧ 𝑣 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) )
24 2 7 10 17 20 22 23 syl132anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( ( 𝑢 Btwn ⟨ 𝑥 , 𝑣 ⟩ ∧ 𝑢 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑥 , 𝑎 ⟩ ∧ 𝑧 Btwn ⟨ 𝑥 , 𝑏 ⟩ ∧ 𝑣 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) )
25 eqid ⊢ ( Base ‘ ( EEG ‘ 𝑁 ) ) = ( Base ‘ ( EEG ‘ 𝑁 ) )
26 eqid ⊢ ( Itv ‘ ( EEG ‘ 𝑁 ) ) = ( Itv ‘ ( EEG ‘ 𝑁 ) )
27 2 25 26 11 21 18 ebtwntg ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( 𝑢 Btwn ⟨ 𝑥 , 𝑣 ⟩ ↔ 𝑢 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑣 ) ) )
28 2 25 26 12 13 18 ebtwntg ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( 𝑢 Btwn ⟨ 𝑦 , 𝑧 ⟩ ↔ 𝑢 ∈ ( 𝑦 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑧 ) ) )
29 27 28 3anbi12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( ( 𝑢 Btwn ⟨ 𝑥 , 𝑣 ⟩ ∧ 𝑢 Btwn ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ≠ 𝑢 ) ↔ ( 𝑢 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) )
30 19 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
31 2 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
32 11 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
33 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) )
34 33 30 eleqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑎 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
35 34 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑎 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
36 12 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
37 31 25 26 32 35 36 ebtwntg ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑦 Btwn ⟨ 𝑥 , 𝑎 ⟩ ↔ 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ) )
38 simpr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
39 19 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
40 38 39 eleqtrd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑏 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
41 13 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
42 31 25 26 32 40 41 ebtwntg ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑧 Btwn ⟨ 𝑥 , 𝑏 ⟩ ↔ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) )
43 21 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
44 31 25 26 35 40 43 ebtwntg ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑣 Btwn ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) )
45 37 42 44 3anbi123d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑦 Btwn ⟨ 𝑥 , 𝑎 ⟩ ∧ 𝑧 Btwn ⟨ 𝑥 , 𝑏 ⟩ ∧ 𝑣 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) ) )
46 30 45 rexeqbidva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑥 , 𝑎 ⟩ ∧ 𝑧 Btwn ⟨ 𝑥 , 𝑏 ⟩ ∧ 𝑣 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ∃ 𝑏 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) ) )
47 19 46 rexeqbidva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑥 , 𝑎 ⟩ ∧ 𝑧 Btwn ⟨ 𝑥 , 𝑏 ⟩ ∧ 𝑣 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ∃ 𝑎 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∃ 𝑏 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) ) )
48 24 29 47 3imtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ( ( 𝑢 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∃ 𝑏 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) ) )
49 48 ralrimivvva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) ) → ∀ 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( ( 𝑢 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∃ 𝑏 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) ) )
50 49 ralrimivva ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( ( 𝑢 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∃ 𝑏 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) ) )
51 eqid ⊢ ( dist ‘ ( EEG ‘ 𝑁 ) ) = ( dist ‘ ( EEG ‘ 𝑁 ) )
52 25 51 26 istrkge ⊢ ( ( EEG ‘ 𝑁 ) ∈ TarskiGE ↔ ( ( EEG ‘ 𝑁 ) ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑦 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑧 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑢 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∀ 𝑣 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( ( 𝑢 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ∃ 𝑏 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ( 𝑦 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 ( Itv ‘ ( EEG ‘ 𝑁 ) ) 𝑏 ) ) ) ) )
53 1 50 52 sylanbrc ⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) ∈ TarskiGE )