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