Step | Hyp | Ref
| Expression |
1 | | fvexd 6732 |
. 2
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
V) |
2 | | simpll 767 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
3 | | simprl 771 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
4 | | eengbas 27072 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
6 | 3, 5 | eleqtrrd 2841 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
7 | 6 | adantr 484 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
8 | | simprr 773 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
9 | 8, 5 | eleqtrrd 2841 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
10 | 9 | adantr 484 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
11 | 3 | adantr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
12 | 8 | adantr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
13 | | simpr1 1196 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
14 | | simpr3 1198 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
15 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
16 | 14, 15 | eleqtrrd 2841 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁)) |
17 | 2, 11, 12, 13, 16 | syl13anc 1374 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁)) |
18 | | simpr2 1197 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (Base‘(EEG‘𝑁))) |
19 | 4 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
20 | 18, 19 | eleqtrrd 2841 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (𝔼‘𝑁)) |
21 | | simpr3 1198 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (Base‘(EEG‘𝑁))) |
22 | 21, 19 | eleqtrrd 2841 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (𝔼‘𝑁)) |
23 | | axeuclid 27054 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ (𝑢 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → ((𝑢 Btwn 〈𝑥, 𝑣〉 ∧ 𝑢 Btwn 〈𝑦, 𝑧〉 ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉))) |
24 | 2, 7, 10, 17, 20, 22, 23 | syl132anc 1390 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn 〈𝑥, 𝑣〉 ∧ 𝑢 Btwn 〈𝑦, 𝑧〉 ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉))) |
25 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(EEG‘𝑁)) = (Base‘(EEG‘𝑁)) |
26 | | eqid 2737 |
. . . . . . 7
⊢
(Itv‘(EEG‘𝑁)) = (Itv‘(EEG‘𝑁)) |
27 | 2, 25, 26, 11, 21, 18 | ebtwntg 27073 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑢 Btwn 〈𝑥, 𝑣〉 ↔ 𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑣))) |
28 | 2, 25, 26, 12, 13, 18 | ebtwntg 27073 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑢 Btwn 〈𝑦, 𝑧〉 ↔ 𝑢 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧))) |
29 | 27, 28 | 3anbi12d 1439 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn 〈𝑥, 𝑣〉 ∧ 𝑢 Btwn 〈𝑦, 𝑧〉 ∧ 𝑥 ≠ 𝑢) ↔ (𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑣) ∧ 𝑢 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑥 ≠ 𝑢))) |
30 | 19 | adantr 484 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
31 | 2 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
32 | 11 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
33 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (𝔼‘𝑁)) |
34 | 33, 30 | eleqtrd 2840 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
35 | 34 | adantr 484 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
36 | 12 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
37 | 31, 25, 26, 32, 35, 36 | ebtwntg 27073 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑦 Btwn 〈𝑥, 𝑎〉 ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑎))) |
38 | | simpr 488 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑏 ∈ (𝔼‘𝑁)) |
39 | 19 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
40 | 38, 39 | eleqtrd 2840 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑏 ∈ (Base‘(EEG‘𝑁))) |
41 | 13 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
42 | 31, 25, 26, 32, 40, 41 | ebtwntg 27073 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑧 Btwn 〈𝑥, 𝑏〉 ↔ 𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑏))) |
43 | 21 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑣 ∈ (Base‘(EEG‘𝑁))) |
44 | 31, 25, 26, 35, 40, 43 | ebtwntg 27073 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑣 Btwn 〈𝑎, 𝑏〉 ↔ 𝑣 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑏))) |
45 | 37, 42, 44 | 3anbi123d 1438 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉) ↔ (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑎) ∧ 𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑏) ∧ 𝑣 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑏)))) |
46 | 30, 45 | rexeqbidva 3332 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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 3332 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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 296 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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 3113 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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 3112 |
. 2
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
(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 2737 |
. . 3
⊢
(dist‘(EEG‘𝑁)) = (dist‘(EEG‘𝑁)) |
52 | 25, 51, 26 | istrkge 26548 |
. 2
⊢
((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 586 |
1
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
TarskiGE) |