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