Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . 3
⊢
(EEG‘𝑁) ∈
V |
2 | 1 | a1i 11 |
. 2
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
V) |
3 | | simpl 472 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
5 | | simprl 790 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
6 | | eengbas 25661 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
8 | 5, 7 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
10 | | simprr 792 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
11 | 10, 7 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
12 | 11 | adantr 480 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
13 | 5 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
14 | 10 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
15 | | simpr1 1060 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
16 | | simpr3 1062 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
17 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
18 | 16, 17 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁)) |
19 | 4, 13, 14, 15, 18 | syl13anc 1320 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁)) |
20 | | simpr2 1061 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (Base‘(EEG‘𝑁))) |
21 | 6 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
22 | 20, 21 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (𝔼‘𝑁)) |
23 | | simpr3 1062 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (Base‘(EEG‘𝑁))) |
24 | 23, 21 | eleqtrrd 2691 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (𝔼‘𝑁)) |
25 | | axeuclid 25643 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ (𝑢 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → ((𝑢 Btwn 〈𝑥, 𝑣〉 ∧ 𝑢 Btwn 〈𝑦, 𝑧〉 ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉))) |
26 | 4, 9, 12, 19, 22, 24, 25 | syl132anc 1336 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn 〈𝑥, 𝑣〉 ∧ 𝑢 Btwn 〈𝑦, 𝑧〉 ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉))) |
27 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(EEG‘𝑁)) = (Base‘(EEG‘𝑁)) |
28 | | eqid 2610 |
. . . . . . 7
⊢
(Itv‘(EEG‘𝑁)) = (Itv‘(EEG‘𝑁)) |
29 | 4, 27, 28, 13, 23, 20 | ebtwntg 25662 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑢 Btwn 〈𝑥, 𝑣〉 ↔ 𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑣))) |
30 | 4, 27, 28, 14, 15, 20 | ebtwntg 25662 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑢 Btwn 〈𝑦, 𝑧〉 ↔ 𝑢 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧))) |
31 | 29, 30 | 3anbi12d 1392 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn 〈𝑥, 𝑣〉 ∧ 𝑢 Btwn 〈𝑦, 𝑧〉 ∧ 𝑥 ≠ 𝑢) ↔ (𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑣) ∧ 𝑢 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑥 ≠ 𝑢))) |
32 | 21 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
33 | 4 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
34 | 13 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
35 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (𝔼‘𝑁)) |
36 | 35, 32 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
37 | 36 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
38 | 14 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
39 | 33, 27, 28, 34, 37, 38 | ebtwntg 25662 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑦 Btwn 〈𝑥, 𝑎〉 ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑎))) |
40 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑏 ∈ (𝔼‘𝑁)) |
41 | 21 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
42 | 40, 41 | eleqtrd 2690 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑏 ∈ (Base‘(EEG‘𝑁))) |
43 | 15 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
44 | 33, 27, 28, 34, 42, 43 | ebtwntg 25662 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑧 Btwn 〈𝑥, 𝑏〉 ↔ 𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑏))) |
45 | 23 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → 𝑣 ∈ (Base‘(EEG‘𝑁))) |
46 | 33, 27, 28, 37, 42, 45 | ebtwntg 25662 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (𝑣 Btwn 〈𝑎, 𝑏〉 ↔ 𝑣 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑏))) |
47 | 39, 44, 46 | 3anbi123d 1391 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ 𝑏 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉) ↔ (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑎) ∧ 𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑏) ∧ 𝑣 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑏)))) |
48 | 32, 47 | rexeqbidva 3132 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (∃𝑏 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉) ↔ ∃𝑏 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑎) ∧ 𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑏) ∧ 𝑣 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑏)))) |
49 | 21, 48 | rexeqbidva 3132 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (𝔼‘𝑁)∃𝑏 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑎〉 ∧ 𝑧 Btwn 〈𝑥, 𝑏〉 ∧ 𝑣 Btwn 〈𝑎, 𝑏〉) ↔ ∃𝑎 ∈ (Base‘(EEG‘𝑁))∃𝑏 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑎) ∧ 𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑏) ∧ 𝑣 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑏)))) |
50 | 26, 31, 49 | 3imtr3d 281 |
. . . 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‘𝑁))𝑏)))) |
51 | 50 | ralrimivvva 2955 |
. . 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‘𝑁))𝑏)))) |
52 | 51 | ralrimivva 2954 |
. 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‘𝑁))𝑏)))) |
53 | | eqid 2610 |
. . 3
⊢
(dist‘(EEG‘𝑁)) = (dist‘(EEG‘𝑁)) |
54 | 27, 53, 28 | istrkge 25156 |
. 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‘𝑁))𝑏))))) |
55 | 2, 52, 54 | sylanbrc 695 |
1
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
TarskiGE) |