Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . . 7
⊢
(EEG‘𝑁) ∈
V |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
V) |
3 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
4 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
5 | | eengbas 25661 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
6 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
7 | 4, 6 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
8 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
9 | 8, 6 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
10 | | axcgrrflx 25594 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) → 〈𝑥, 𝑦〉Cgr〈𝑦, 𝑥〉) |
11 | 3, 7, 9, 10 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → 〈𝑥, 𝑦〉Cgr〈𝑦, 𝑥〉) |
12 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(EEG‘𝑁)) = (Base‘(EEG‘𝑁)) |
13 | | eqid 2610 |
. . . . . . . . 9
⊢
(dist‘(EEG‘𝑁)) = (dist‘(EEG‘𝑁)) |
14 | 3, 12, 13, 4, 8, 8,
4 | ecgrtg 25663 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (〈𝑥, 𝑦〉Cgr〈𝑦, 𝑥〉 ↔ (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥))) |
15 | 11, 14 | mpbid 221 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥)) |
16 | 15 | ralrimivva 2954 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
(Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥)) |
17 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
18 | | simpr1 1060 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
19 | | simpr2 1061 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
20 | | simpr3 1062 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
21 | 17, 12, 13, 18, 19, 20, 20 | ecgrtg 25663 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → (〈𝑥, 𝑦〉Cgr〈𝑧, 𝑧〉 ↔ (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧))) |
22 | 7 | 3adantr3 1215 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
23 | 9 | 3adantr3 1215 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
24 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
25 | 20, 24 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁)) |
26 | | axcgrid 25596 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → (〈𝑥, 𝑦〉Cgr〈𝑧, 𝑧〉 → 𝑥 = 𝑦)) |
27 | 17, 22, 23, 25, 26 | syl13anc 1320 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → (〈𝑥, 𝑦〉Cgr〈𝑧, 𝑧〉 → 𝑥 = 𝑦)) |
28 | 21, 27 | sylbird 249 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁))
∧ 𝑧 ∈
(Base‘(EEG‘𝑁)))) → ((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦)) |
29 | 28 | ralrimivvva 2955 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
(Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦)) |
30 | 2, 16, 29 | jca32 556 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((EEG‘𝑁) ∈ V
∧ (∀𝑥 ∈
(Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦)))) |
31 | | eqid 2610 |
. . . . . 6
⊢
(Itv‘(EEG‘𝑁)) = (Itv‘(EEG‘𝑁)) |
32 | 12, 13, 31 | istrkgc 25153 |
. . . . 5
⊢
((EEG‘𝑁)
∈ TarskiGC ↔ ((EEG‘𝑁) ∈ V ∧ (∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑦(dist‘(EEG‘𝑁))𝑥) ∧ ∀𝑥 ∈ (Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))((𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑧(dist‘(EEG‘𝑁))𝑧) → 𝑥 = 𝑦)))) |
33 | 30, 32 | sylibr 223 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
TarskiGC) |
34 | 3, 12, 31, 4, 4, 8 | ebtwntg 25662 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝑦 Btwn 〈𝑥, 𝑥〉 ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥))) |
35 | | axbtwnid 25619 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑦 Btwn 〈𝑥, 𝑥〉 → 𝑦 = 𝑥)) |
36 | 3, 9, 7, 35 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝑦 Btwn 〈𝑥, 𝑥〉 → 𝑦 = 𝑥)) |
37 | 34, 36 | sylbird 249 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑦 = 𝑥)) |
38 | 37 | imp 444 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥)) → 𝑦 = 𝑥) |
39 | 38 | eqcomd 2616 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥)) → 𝑥 = 𝑦) |
40 | 39 | ex 449 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑥 = 𝑦)) |
41 | 40 | ralrimivva 2954 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
(Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑥) → 𝑥 = 𝑦)) |
42 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
43 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
44 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
45 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
46 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
47 | | simpr1 1060 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
48 | 42, 45, 46, 47, 25 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁)) |
49 | | simpr2 1061 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (Base‘(EEG‘𝑁))) |
50 | 42, 5 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
51 | 49, 50 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (𝔼‘𝑁)) |
52 | | simpr3 1062 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (Base‘(EEG‘𝑁))) |
53 | 52, 50 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (𝔼‘𝑁)) |
54 | | axpasch 25621 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ (𝑢 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → ((𝑢 Btwn 〈𝑥, 𝑧〉 ∧ 𝑣 Btwn 〈𝑦, 𝑧〉) → ∃𝑎 ∈ (𝔼‘𝑁)(𝑎 Btwn 〈𝑢, 𝑦〉 ∧ 𝑎 Btwn 〈𝑣, 𝑥〉))) |
55 | 42, 43, 44, 48, 51, 53, 54 | syl132anc 1336 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn 〈𝑥, 𝑧〉 ∧ 𝑣 Btwn 〈𝑦, 𝑧〉) → ∃𝑎 ∈ (𝔼‘𝑁)(𝑎 Btwn 〈𝑢, 𝑦〉 ∧ 𝑎 Btwn 〈𝑣, 𝑥〉))) |
56 | 42, 12, 31, 45, 47, 49 | ebtwntg 25662 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑢 Btwn 〈𝑥, 𝑧〉 ↔ 𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧))) |
57 | 42, 12, 31, 46, 47, 52 | ebtwntg 25662 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑣 Btwn 〈𝑦, 𝑧〉 ↔ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧))) |
58 | 56, 57 | anbi12d 743 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 Btwn 〈𝑥, 𝑧〉 ∧ 𝑣 Btwn 〈𝑦, 𝑧〉) ↔ (𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)))) |
59 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
60 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑢 ∈ (Base‘(EEG‘𝑁))) |
61 | 46 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
62 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (𝔼‘𝑁)) |
63 | 50 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
64 | 62, 63 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
65 | 59, 12, 31, 60, 61, 64 | ebtwntg 25662 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝑎 Btwn 〈𝑢, 𝑦〉 ↔ 𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦))) |
66 | 52 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑣 ∈ (Base‘(EEG‘𝑁))) |
67 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
68 | 59, 12, 31, 66, 67, 64 | ebtwntg 25662 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (𝑎 Btwn 〈𝑣, 𝑥〉 ↔ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥))) |
69 | 65, 68 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → ((𝑎 Btwn 〈𝑢, 𝑦〉 ∧ 𝑎 Btwn 〈𝑣, 𝑥〉) ↔ (𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥)))) |
70 | 50, 69 | rexeqbidva 3132 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (𝔼‘𝑁)(𝑎 Btwn 〈𝑢, 𝑦〉 ∧ 𝑎 Btwn 〈𝑣, 𝑥〉) ↔ ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥)))) |
71 | 55, 58, 70 | 3imtr3d 281 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥)))) |
72 | 71 | ralrimivvva 2955 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → ∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥)))) |
73 | 72 | ralrimivva 2954 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
(Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑧 ∈ (Base‘(EEG‘𝑁))∀𝑢 ∈ (Base‘(EEG‘𝑁))∀𝑣 ∈ (Base‘(EEG‘𝑁))((𝑢 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑣 ∈ (𝑦(Itv‘(EEG‘𝑁))𝑧)) → ∃𝑎 ∈ (Base‘(EEG‘𝑁))(𝑎 ∈ (𝑢(Itv‘(EEG‘𝑁))𝑦) ∧ 𝑎 ∈ (𝑣(Itv‘(EEG‘𝑁))𝑥)))) |
74 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
75 | | elpwi 4117 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
→ 𝑠 ⊆
(Base‘(EEG‘𝑁))) |
76 | 75 | ad2antrl 760 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → 𝑠 ⊆ (Base‘(EEG‘𝑁))) |
77 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
78 | 76, 77 | sseqtr4d 3605 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → 𝑠 ⊆ (𝔼‘𝑁)) |
79 | | elpwi 4117 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁))
→ 𝑡 ⊆
(Base‘(EEG‘𝑁))) |
80 | 79 | ad2antll 761 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → 𝑡 ⊆ (Base‘(EEG‘𝑁))) |
81 | 80, 77 | sseqtr4d 3605 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → 𝑡 ⊆ (𝔼‘𝑁)) |
82 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉) → 𝑁 ∈ ℕ) |
83 | | simplrl 796 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉) → 𝑠 ⊆ (𝔼‘𝑁)) |
84 | | simplrr 797 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉) → 𝑡 ⊆ (𝔼‘𝑁)) |
85 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉) → ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉) |
86 | | axcont 25656 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉)) → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 Btwn 〈𝑥, 𝑦〉) |
87 | 82, 83, 84, 85, 86 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) ∧ ∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉) → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 Btwn 〈𝑥, 𝑦〉) |
88 | 87 | ex 449 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ⊆ (𝔼‘𝑁) ∧ 𝑡 ⊆ (𝔼‘𝑁))) → (∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉 → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 Btwn 〈𝑥, 𝑦〉)) |
89 | 74, 78, 81, 88 | syl12anc 1316 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉 → ∃𝑏 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 Btwn 〈𝑥, 𝑦〉)) |
90 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑁 ∈ ℕ) |
91 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑎 ∈ (𝔼‘𝑁)) |
92 | 77 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
93 | 91, 92 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
94 | 80 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ (Base‘(EEG‘𝑁))) |
95 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡) |
96 | 94, 95 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
97 | 76 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ (Base‘(EEG‘𝑁))) |
98 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠) |
99 | 97, 98 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
100 | 90, 12, 31, 93, 96, 99 | ebtwntg 25662 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝑥 Btwn 〈𝑎, 𝑦〉 ↔ 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦))) |
101 | 100 | 2ralbidva 2971 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑎 ∈ (𝔼‘𝑁)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉 ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦))) |
102 | 77, 101 | rexeqbidva 3132 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 Btwn 〈𝑎, 𝑦〉 ↔ ∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦))) |
103 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑁 ∈ ℕ) |
104 | 76 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ (Base‘(EEG‘𝑁))) |
105 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠) |
106 | 104, 105 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
107 | 80 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ (Base‘(EEG‘𝑁))) |
108 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡) |
109 | 107, 108 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
110 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑏 ∈ (𝔼‘𝑁)) |
111 | 77 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
112 | 110, 111 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑏 ∈ (Base‘(EEG‘𝑁))) |
113 | 103, 12, 31, 106, 109, 112 | ebtwntg 25662 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝑏 Btwn 〈𝑥, 𝑦〉 ↔ 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦))) |
114 | 113 | 2ralbidva 2971 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) ∧ 𝑏 ∈ (𝔼‘𝑁)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 Btwn 〈𝑥, 𝑦〉 ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦))) |
115 | 77, 114 | rexeqbidva 3132 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → (∃𝑏 ∈ (𝔼‘𝑁)∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 Btwn 〈𝑥, 𝑦〉 ↔ ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦))) |
116 | 89, 102, 115 | 3imtr3d 281 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))
∧ 𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁)))) → (∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦) → ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦))) |
117 | 116 | ralrimivva 2954 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑠 ∈ 𝒫
(Base‘(EEG‘𝑁))∀𝑡 ∈ 𝒫
(Base‘(EEG‘𝑁))(∃𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑦) → ∃𝑏 ∈ (Base‘(EEG‘𝑁))∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦))) |
118 | 41, 73, 117 | 3jca 1235 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(∀𝑥 ∈
(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 | 12, 13, 31 | istrkgb 25154 |
. . . . 5
⊢
((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‘𝑁))𝑦))))) |
120 | 2, 118, 119 | sylanbrc 695 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
TarskiGB) |
121 | 33, 120 | elind 3760 |
. . 3
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
(TarskiGC ∩ TarskiGB)) |
122 | | simplll 794 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
123 | 4 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
124 | 122, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
125 | 123, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
126 | 8 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
127 | 126, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
128 | | simplr1 1096 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
129 | 128, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑧 ∈ (𝔼‘𝑁)) |
130 | | simplr2 1097 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (Base‘(EEG‘𝑁))) |
131 | 130, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑢 ∈ (𝔼‘𝑁)) |
132 | | simplr3 1098 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
133 | 132, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (𝔼‘𝑁)) |
134 | | simpr1 1060 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (Base‘(EEG‘𝑁))) |
135 | 134, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (𝔼‘𝑁)) |
136 | | simpr2 1061 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑐 ∈ (Base‘(EEG‘𝑁))) |
137 | 136, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑐 ∈ (𝔼‘𝑁)) |
138 | | simpr3 1062 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (Base‘(EEG‘𝑁))) |
139 | 138, 124 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → 𝑣 ∈ (𝔼‘𝑁)) |
140 | | 3anass 1035 |
. . . . . . . . . . . 12
⊢ (((𝑥 ≠ 𝑦 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 𝑏 Btwn 〈𝑎, 𝑐〉) ∧ (〈𝑥, 𝑦〉Cgr〈𝑎, 𝑏〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑏, 𝑐〉) ∧ (〈𝑥, 𝑢〉Cgr〈𝑎, 𝑣〉 ∧ 〈𝑦, 𝑢〉Cgr〈𝑏, 𝑣〉)) ↔ ((𝑥 ≠ 𝑦 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 𝑏 Btwn 〈𝑎, 𝑐〉) ∧ ((〈𝑥, 𝑦〉Cgr〈𝑎, 𝑏〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑏, 𝑐〉) ∧ (〈𝑥, 𝑢〉Cgr〈𝑎, 𝑣〉 ∧ 〈𝑦, 𝑢〉Cgr〈𝑏, 𝑣〉)))) |
141 | | ax5seg 25618 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑧 ∈ (𝔼‘𝑁) ∧ 𝑢 ∈ (𝔼‘𝑁) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → (((𝑥 ≠ 𝑦 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 𝑏 Btwn 〈𝑎, 𝑐〉) ∧ (〈𝑥, 𝑦〉Cgr〈𝑎, 𝑏〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑏, 𝑐〉) ∧ (〈𝑥, 𝑢〉Cgr〈𝑎, 𝑣〉 ∧ 〈𝑦, 𝑢〉Cgr〈𝑏, 𝑣〉)) → 〈𝑧, 𝑢〉Cgr〈𝑐, 𝑣〉)) |
142 | 140, 141 | syl5bir 232 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑧 ∈ (𝔼‘𝑁) ∧ 𝑢 ∈ (𝔼‘𝑁) ∧ 𝑎 ∈ (𝔼‘𝑁)) ∧ (𝑏 ∈ (𝔼‘𝑁) ∧ 𝑐 ∈ (𝔼‘𝑁) ∧ 𝑣 ∈ (𝔼‘𝑁))) → (((𝑥 ≠ 𝑦 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 𝑏 Btwn 〈𝑎, 𝑐〉) ∧ ((〈𝑥, 𝑦〉Cgr〈𝑎, 𝑏〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑏, 𝑐〉) ∧ (〈𝑥, 𝑢〉Cgr〈𝑎, 𝑣〉 ∧ 〈𝑦, 𝑢〉Cgr〈𝑏, 𝑣〉))) → 〈𝑧, 𝑢〉Cgr〈𝑐, 𝑣〉)) |
143 | 122, 125,
127, 129, 131, 133, 135, 137, 139, 142 | syl333anc 1350 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (((𝑥 ≠ 𝑦 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 𝑏 Btwn 〈𝑎, 𝑐〉) ∧ ((〈𝑥, 𝑦〉Cgr〈𝑎, 𝑏〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑏, 𝑐〉) ∧ (〈𝑥, 𝑢〉Cgr〈𝑎, 𝑣〉 ∧ 〈𝑦, 𝑢〉Cgr〈𝑏, 𝑣〉))) → 〈𝑧, 𝑢〉Cgr〈𝑐, 𝑣〉)) |
144 | 122, 12, 31, 123, 128, 126 | ebtwntg 25662 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑦 Btwn 〈𝑥, 𝑧〉 ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧))) |
145 | 122, 12, 31, 132, 136, 134 | ebtwntg 25662 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (𝑏 Btwn 〈𝑎, 𝑐〉 ↔ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐))) |
146 | 144, 145 | 3anbi23d 1394 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → ((𝑥 ≠ 𝑦 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 𝑏 Btwn 〈𝑎, 𝑐〉) ↔ (𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ 𝑏 ∈ (𝑎(Itv‘(EEG‘𝑁))𝑐)))) |
147 | 122, 12, 13, 123, 126, 132, 134 | ecgrtg 25663 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (〈𝑥, 𝑦〉Cgr〈𝑎, 𝑏〉 ↔ (𝑥(dist‘(EEG‘𝑁))𝑦) = (𝑎(dist‘(EEG‘𝑁))𝑏))) |
148 | 122, 12, 13, 126, 128, 134, 136 | ecgrtg 25663 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (〈𝑦, 𝑧〉Cgr〈𝑏, 𝑐〉 ↔ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑏(dist‘(EEG‘𝑁))𝑐))) |
149 | 147, 148 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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‘𝑁))𝑐)))) |
150 | 122, 12, 13, 123, 130, 132, 138 | ecgrtg 25663 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (〈𝑥, 𝑢〉Cgr〈𝑎, 𝑣〉 ↔ (𝑥(dist‘(EEG‘𝑁))𝑢) = (𝑎(dist‘(EEG‘𝑁))𝑣))) |
151 | 122, 12, 13, 126, 130, 134, 138 | ecgrtg 25663 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (〈𝑦, 𝑢〉Cgr〈𝑏, 𝑣〉 ↔ (𝑦(dist‘(EEG‘𝑁))𝑢) = (𝑏(dist‘(EEG‘𝑁))𝑣))) |
152 | 150, 151 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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‘𝑁))𝑣)))) |
153 | 149, 152 | anbi12d 743 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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‘𝑁))𝑣))))) |
154 | 146, 153 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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‘𝑁))𝑣)))))) |
155 | 122, 12, 13, 128, 130, 136, 138 | ecgrtg 25663 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑧 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑢 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑎 ∈ (Base‘(EEG‘𝑁)))) ∧ (𝑏 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑐 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑣 ∈ (Base‘(EEG‘𝑁)))) → (〈𝑧, 𝑢〉Cgr〈𝑐, 𝑣〉 ↔ (𝑧(dist‘(EEG‘𝑁))𝑢) = (𝑐(dist‘(EEG‘𝑁))𝑣))) |
156 | 143, 154,
155 | 3imtr3d 281 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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 2955 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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 | ralrimivvva 2955 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(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 | 158 | ralrimivva 2954 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
(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‘𝑁))𝑣))) |
160 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑁 ∈ ℕ) |
161 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑥 ∈ (𝔼‘𝑁)) |
162 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑦 ∈ (𝔼‘𝑁)) |
163 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
164 | 160, 5 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) →
(𝔼‘𝑁) =
(Base‘(EEG‘𝑁))) |
165 | 163, 164 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑎 ∈ (𝔼‘𝑁)) |
166 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (Base‘(EEG‘𝑁))) |
167 | 166, 164 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → 𝑏 ∈ (𝔼‘𝑁)) |
168 | | axsegcon 25607 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁)) ∧ (𝑎 ∈ (𝔼‘𝑁) ∧ 𝑏 ∈ (𝔼‘𝑁))) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑎, 𝑏〉)) |
169 | 160, 161,
162, 165, 167, 168 | syl122anc 1327 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → ∃𝑧 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑎, 𝑏〉)) |
170 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑁 ∈ ℕ) |
171 | 4 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (Base‘(EEG‘𝑁))) |
172 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑧 ∈ (𝔼‘𝑁)) |
173 | 164 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (𝔼‘𝑁) = (Base‘(EEG‘𝑁))) |
174 | 172, 173 | eleqtrd 2690 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑧 ∈ (Base‘(EEG‘𝑁))) |
175 | 8 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑦 ∈ (Base‘(EEG‘𝑁))) |
176 | 170, 12, 31, 171, 174, 175 | ebtwntg 25662 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (𝑦 Btwn 〈𝑥, 𝑧〉 ↔ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧))) |
177 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑎 ∈ (Base‘(EEG‘𝑁))) |
178 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → 𝑏 ∈ (Base‘(EEG‘𝑁))) |
179 | 170, 12, 13, 175, 174, 177, 178 | ecgrtg 25663 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (〈𝑦, 𝑧〉Cgr〈𝑎, 𝑏〉 ↔ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏))) |
180 | 176, 179 | anbi12d 743 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) ∧ 𝑧 ∈ (𝔼‘𝑁)) → ((𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑎, 𝑏〉) ↔ (𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))) |
181 | 164, 180 | rexeqbidva 3132 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → (∃𝑧 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝑥, 𝑧〉 ∧ 〈𝑦, 𝑧〉Cgr〈𝑎, 𝑏〉) ↔ ∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏)))) |
182 | 169, 181 | mpbid 221 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) ∧ (𝑎 ∈ (Base‘(EEG‘𝑁)) ∧ 𝑏 ∈ (Base‘(EEG‘𝑁)))) → ∃𝑧 ∈
(Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏))) |
183 | 182 | ralrimivva 2954 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑥 ∈
(Base‘(EEG‘𝑁))
∧ 𝑦 ∈
(Base‘(EEG‘𝑁)))) → ∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏))) |
184 | 183 | ralrimivva 2954 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑥 ∈
(Base‘(EEG‘𝑁))∀𝑦 ∈ (Base‘(EEG‘𝑁))∀𝑎 ∈ (Base‘(EEG‘𝑁))∀𝑏 ∈ (Base‘(EEG‘𝑁))∃𝑧 ∈ (Base‘(EEG‘𝑁))(𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧) ∧ (𝑦(dist‘(EEG‘𝑁))𝑧) = (𝑎(dist‘(EEG‘𝑁))𝑏))) |
185 | 2, 159, 184 | jca32 556 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
((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 | 12, 13, 31 | istrkgcb 25155 |
. . . . 5
⊢
((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‘𝑁))𝑏))))) |
187 | 185, 186 | sylibr 223 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
TarskiGCB) |
188 | 12, 31 | elntg 25664 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(LineG‘(EEG‘𝑁))
= (𝑥 ∈
(Base‘(EEG‘𝑁)),
𝑦 ∈
((Base‘(EEG‘𝑁))
∖ {𝑥}) ↦ {𝑧 ∈
(Base‘(EEG‘𝑁))
∣ (𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧))})) |
189 | 12, 13, 31 | istrkgl 25157 |
. . . . 5
⊢
((EEG‘𝑁)
∈ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ ((EEG‘𝑁) ∈ V ∧
(LineG‘(EEG‘𝑁))
= (𝑥 ∈
(Base‘(EEG‘𝑁)),
𝑦 ∈
((Base‘(EEG‘𝑁))
∖ {𝑥}) ↦ {𝑧 ∈
(Base‘(EEG‘𝑁))
∣ (𝑧 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘(EEG‘𝑁))𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘(EEG‘𝑁))𝑧))}))) |
190 | 2, 188, 189 | sylanbrc 695 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) |
191 | 187, 190 | elind 3760 |
. . 3
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
(TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
192 | 121, 191 | elind 3760 |
. 2
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB
∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))) |
193 | | df-trkg 25152 |
. 2
⊢ TarskiG =
((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB
∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
194 | 192, 193 | syl6eleqr 2699 |
1
⊢ (𝑁 ∈ ℕ →
(EEG‘𝑁) ∈
TarskiG) |