| Step | Hyp | Ref
| Expression |
| 1 | | df-colinear 36040 |
. 2
⊢ Colinear
= ◡{〈〈𝑏, 𝑐〉, 𝑎〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))} |
| 2 | | nnex 12272 |
. . . . 5
⊢ ℕ
∈ V |
| 3 | | fvex 6919 |
. . . . . . 7
⊢
(𝔼‘𝑛)
∈ V |
| 4 | 3, 3 | xpex 7773 |
. . . . . 6
⊢
((𝔼‘𝑛)
× (𝔼‘𝑛))
∈ V |
| 5 | 4, 3 | xpex 7773 |
. . . . 5
⊢
(((𝔼‘𝑛)
× (𝔼‘𝑛))
× (𝔼‘𝑛))
∈ V |
| 6 | 2, 5 | iunex 7993 |
. . . 4
⊢ ∪ 𝑛 ∈ ℕ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛)) ∈ V |
| 7 | | df-oprab 7435 |
. . . . 5
⊢
{〈〈𝑏,
𝑐〉, 𝑎〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))} = {𝑥 ∣ ∃𝑏∃𝑐∃𝑎(𝑥 = 〈〈𝑏, 𝑐〉, 𝑎〉 ∧ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉)))} |
| 8 | | opelxpi 5722 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) → 〈𝑏, 𝑐〉 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) |
| 9 | 8 | 3adant1 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) → 〈𝑏, 𝑐〉 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))) |
| 10 | | simp1 1137 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) → 𝑎 ∈ (𝔼‘𝑛)) |
| 11 | | opelxpi 5722 |
. . . . . . . . . . . . 13
⊢
((〈𝑏, 𝑐〉 ∈
((𝔼‘𝑛) ×
(𝔼‘𝑛)) ∧
𝑎 ∈
(𝔼‘𝑛)) →
〈〈𝑏, 𝑐〉, 𝑎〉 ∈ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛))) |
| 12 | 9, 10, 11 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) → 〈〈𝑏, 𝑐〉, 𝑎〉 ∈ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛))) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉)) → 〈〈𝑏, 𝑐〉, 𝑎〉 ∈ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛))) |
| 14 | 13 | reximi 3084 |
. . . . . . . . . 10
⊢
(∃𝑛 ∈
ℕ ((𝑎 ∈
(𝔼‘𝑛) ∧
𝑏 ∈
(𝔼‘𝑛) ∧
𝑐 ∈
(𝔼‘𝑛)) ∧
(𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉)) → ∃𝑛 ∈ ℕ 〈〈𝑏, 𝑐〉, 𝑎〉 ∈ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛))) |
| 15 | | eliun 4995 |
. . . . . . . . . 10
⊢
(〈〈𝑏,
𝑐〉, 𝑎〉 ∈ ∪ 𝑛 ∈ ℕ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛)) ↔ ∃𝑛 ∈ ℕ
〈〈𝑏, 𝑐〉, 𝑎〉 ∈ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛))) |
| 16 | 14, 15 | sylibr 234 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
ℕ ((𝑎 ∈
(𝔼‘𝑛) ∧
𝑏 ∈
(𝔼‘𝑛) ∧
𝑐 ∈
(𝔼‘𝑛)) ∧
(𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉)) → 〈〈𝑏, 𝑐〉, 𝑎〉 ∈ ∪ 𝑛 ∈ ℕ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛))) |
| 17 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑥 = 〈〈𝑏, 𝑐〉, 𝑎〉 → (𝑥 ∈ ∪
𝑛 ∈ ℕ
(((𝔼‘𝑛)
× (𝔼‘𝑛))
× (𝔼‘𝑛))
↔ 〈〈𝑏, 𝑐〉, 𝑎〉 ∈ ∪ 𝑛 ∈ ℕ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛)))) |
| 18 | 17 | biimpar 477 |
. . . . . . . . 9
⊢ ((𝑥 = 〈〈𝑏, 𝑐〉, 𝑎〉 ∧ 〈〈𝑏, 𝑐〉, 𝑎〉 ∈ ∪ 𝑛 ∈ ℕ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛))) → 𝑥 ∈ ∪
𝑛 ∈ ℕ
(((𝔼‘𝑛)
× (𝔼‘𝑛))
× (𝔼‘𝑛))) |
| 19 | 16, 18 | sylan2 593 |
. . . . . . . 8
⊢ ((𝑥 = 〈〈𝑏, 𝑐〉, 𝑎〉 ∧ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))) → 𝑥 ∈ ∪
𝑛 ∈ ℕ
(((𝔼‘𝑛)
× (𝔼‘𝑛))
× (𝔼‘𝑛))) |
| 20 | 19 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑎(𝑥 = 〈〈𝑏, 𝑐〉, 𝑎〉 ∧ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))) → 𝑥 ∈ ∪
𝑛 ∈ ℕ
(((𝔼‘𝑛)
× (𝔼‘𝑛))
× (𝔼‘𝑛))) |
| 21 | 20 | exlimivv 1932 |
. . . . . 6
⊢
(∃𝑏∃𝑐∃𝑎(𝑥 = 〈〈𝑏, 𝑐〉, 𝑎〉 ∧ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))) → 𝑥 ∈ ∪
𝑛 ∈ ℕ
(((𝔼‘𝑛)
× (𝔼‘𝑛))
× (𝔼‘𝑛))) |
| 22 | 21 | abssi 4070 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑏∃𝑐∃𝑎(𝑥 = 〈〈𝑏, 𝑐〉, 𝑎〉 ∧ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉)))} ⊆ ∪ 𝑛 ∈ ℕ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛)) |
| 23 | 7, 22 | eqsstri 4030 |
. . . 4
⊢
{〈〈𝑏,
𝑐〉, 𝑎〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))} ⊆ ∪ 𝑛 ∈ ℕ (((𝔼‘𝑛) × (𝔼‘𝑛)) × (𝔼‘𝑛)) |
| 24 | 6, 23 | ssexi 5322 |
. . 3
⊢
{〈〈𝑏,
𝑐〉, 𝑎〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))} ∈ V |
| 25 | 24 | cnvex 7947 |
. 2
⊢ ◡{〈〈𝑏, 𝑐〉, 𝑎〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑐 ∈ (𝔼‘𝑛)) ∧ (𝑎 Btwn 〈𝑏, 𝑐〉 ∨ 𝑏 Btwn 〈𝑐, 𝑎〉 ∨ 𝑐 Btwn 〈𝑎, 𝑏〉))} ∈ V |
| 26 | 1, 25 | eqeltri 2837 |
1
⊢ Colinear
∈ V |