Step | Hyp | Ref
| Expression |
1 | | colinrel 34359 |
. . . 4
⊢ Rel
Colinear |
2 | 1 | brrelex1i 5643 |
. . 3
⊢ (𝑃 Colinear 〈𝑄, 𝑅〉 → 𝑃 ∈ V) |
3 | 2 | a1i 11 |
. 2
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑃 Colinear 〈𝑄, 𝑅〉 → 𝑃 ∈ V)) |
4 | | elex 3450 |
. . . . . 6
⊢ (𝑃 ∈ (𝔼‘𝑛) → 𝑃 ∈ V) |
5 | 4 | 3ad2ant1 1132 |
. . . . 5
⊢ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) → 𝑃 ∈ V) |
6 | 5 | adantr 481 |
. . . 4
⊢ (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)) → 𝑃 ∈ V) |
7 | 6 | rexlimivw 3211 |
. . 3
⊢
(∃𝑛 ∈
ℕ ((𝑃 ∈
(𝔼‘𝑛) ∧
𝑄 ∈
(𝔼‘𝑛) ∧
𝑅 ∈
(𝔼‘𝑛)) ∧
(𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)) → 𝑃 ∈ V) |
8 | 7 | a1i 11 |
. 2
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)) → 𝑃 ∈ V)) |
9 | | df-br 5075 |
. . . . . 6
⊢ (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ 〈𝑃, 〈𝑄, 𝑅〉〉 ∈ Colinear
) |
10 | | df-colinear 34341 |
. . . . . . 7
⊢ Colinear
= ◡{〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))} |
11 | 10 | eleq2i 2830 |
. . . . . 6
⊢
(〈𝑃,
〈𝑄, 𝑅〉〉 ∈ Colinear ↔
〈𝑃, 〈𝑄, 𝑅〉〉 ∈ ◡{〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))}) |
12 | 9, 11 | bitri 274 |
. . . . 5
⊢ (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ 〈𝑃, 〈𝑄, 𝑅〉〉 ∈ ◡{〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))}) |
13 | | opex 5379 |
. . . . . . 7
⊢
〈𝑄, 𝑅〉 ∈ V |
14 | | opelcnvg 5789 |
. . . . . . 7
⊢ ((𝑃 ∈ V ∧ 〈𝑄, 𝑅〉 ∈ V) → (〈𝑃, 〈𝑄, 𝑅〉〉 ∈ ◡{〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))} ↔ 〈〈𝑄, 𝑅〉, 𝑃〉 ∈ {〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))})) |
15 | 13, 14 | mpan2 688 |
. . . . . 6
⊢ (𝑃 ∈ V → (〈𝑃, 〈𝑄, 𝑅〉〉 ∈ ◡{〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))} ↔ 〈〈𝑄, 𝑅〉, 𝑃〉 ∈ {〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))})) |
16 | 15 | 3ad2ant3 1134 |
. . . . 5
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V) → (〈𝑃, 〈𝑄, 𝑅〉〉 ∈ ◡{〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))} ↔ 〈〈𝑄, 𝑅〉, 𝑃〉 ∈ {〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))})) |
17 | 12, 16 | syl5bb 283 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V) → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ 〈〈𝑄, 𝑅〉, 𝑃〉 ∈ {〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))})) |
18 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑞 = 𝑄 → (𝑞 ∈ (𝔼‘𝑛) ↔ 𝑄 ∈ (𝔼‘𝑛))) |
19 | 18 | 3anbi2d 1440 |
. . . . . . 7
⊢ (𝑞 = 𝑄 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ↔ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)))) |
20 | | opeq1 4804 |
. . . . . . . . 9
⊢ (𝑞 = 𝑄 → 〈𝑞, 𝑟〉 = 〈𝑄, 𝑟〉) |
21 | 20 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑞 = 𝑄 → (𝑝 Btwn 〈𝑞, 𝑟〉 ↔ 𝑝 Btwn 〈𝑄, 𝑟〉)) |
22 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑞 = 𝑄 → (𝑞 Btwn 〈𝑟, 𝑝〉 ↔ 𝑄 Btwn 〈𝑟, 𝑝〉)) |
23 | | opeq2 4805 |
. . . . . . . . 9
⊢ (𝑞 = 𝑄 → 〈𝑝, 𝑞〉 = 〈𝑝, 𝑄〉) |
24 | 23 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑞 = 𝑄 → (𝑟 Btwn 〈𝑝, 𝑞〉 ↔ 𝑟 Btwn 〈𝑝, 𝑄〉)) |
25 | 21, 22, 24 | 3orbi123d 1434 |
. . . . . . 7
⊢ (𝑞 = 𝑄 → ((𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉) ↔ (𝑝 Btwn 〈𝑄, 𝑟〉 ∨ 𝑄 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑄〉))) |
26 | 19, 25 | anbi12d 631 |
. . . . . 6
⊢ (𝑞 = 𝑄 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉)) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑟〉 ∨ 𝑄 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑄〉)))) |
27 | 26 | rexbidv 3226 |
. . . . 5
⊢ (𝑞 = 𝑄 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉)) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑟〉 ∨ 𝑄 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑄〉)))) |
28 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑟 ∈ (𝔼‘𝑛) ↔ 𝑅 ∈ (𝔼‘𝑛))) |
29 | 28 | 3anbi3d 1441 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ↔ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)))) |
30 | | opeq2 4805 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → 〈𝑄, 𝑟〉 = 〈𝑄, 𝑅〉) |
31 | 30 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑝 Btwn 〈𝑄, 𝑟〉 ↔ 𝑝 Btwn 〈𝑄, 𝑅〉)) |
32 | | opeq1 4804 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → 〈𝑟, 𝑝〉 = 〈𝑅, 𝑝〉) |
33 | 32 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑄 Btwn 〈𝑟, 𝑝〉 ↔ 𝑄 Btwn 〈𝑅, 𝑝〉)) |
34 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑟 Btwn 〈𝑝, 𝑄〉 ↔ 𝑅 Btwn 〈𝑝, 𝑄〉)) |
35 | 31, 33, 34 | 3orbi123d 1434 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ((𝑝 Btwn 〈𝑄, 𝑟〉 ∨ 𝑄 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑄〉) ↔ (𝑝 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑝〉 ∨ 𝑅 Btwn 〈𝑝, 𝑄〉))) |
36 | 29, 35 | anbi12d 631 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑟〉 ∨ 𝑄 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑄〉)) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑝〉 ∨ 𝑅 Btwn 〈𝑝, 𝑄〉)))) |
37 | 36 | rexbidv 3226 |
. . . . 5
⊢ (𝑟 = 𝑅 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑟〉 ∨ 𝑄 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑄〉)) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑝〉 ∨ 𝑅 Btwn 〈𝑝, 𝑄〉)))) |
38 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝 ∈ (𝔼‘𝑛) ↔ 𝑃 ∈ (𝔼‘𝑛))) |
39 | 38 | 3anbi1d 1439 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ↔ (𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)))) |
40 | | breq1 5077 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝 Btwn 〈𝑄, 𝑅〉 ↔ 𝑃 Btwn 〈𝑄, 𝑅〉)) |
41 | | opeq2 4805 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → 〈𝑅, 𝑝〉 = 〈𝑅, 𝑃〉) |
42 | 41 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑄 Btwn 〈𝑅, 𝑝〉 ↔ 𝑄 Btwn 〈𝑅, 𝑃〉)) |
43 | | opeq1 4804 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → 〈𝑝, 𝑄〉 = 〈𝑃, 𝑄〉) |
44 | 43 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑅 Btwn 〈𝑝, 𝑄〉 ↔ 𝑅 Btwn 〈𝑃, 𝑄〉)) |
45 | 40, 42, 44 | 3orbi123d 1434 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → ((𝑝 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑝〉 ∨ 𝑅 Btwn 〈𝑝, 𝑄〉) ↔ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉))) |
46 | 39, 45 | anbi12d 631 |
. . . . . 6
⊢ (𝑝 = 𝑃 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑝〉 ∨ 𝑅 Btwn 〈𝑝, 𝑄〉)) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) |
47 | 46 | rexbidv 3226 |
. . . . 5
⊢ (𝑝 = 𝑃 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑝〉 ∨ 𝑅 Btwn 〈𝑝, 𝑄〉)) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) |
48 | 27, 37, 47 | eloprabg 7384 |
. . . 4
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V) → (〈〈𝑄, 𝑅〉, 𝑃〉 ∈ {〈〈𝑞, 𝑟〉, 𝑝〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn 〈𝑞, 𝑟〉 ∨ 𝑞 Btwn 〈𝑟, 𝑝〉 ∨ 𝑟 Btwn 〈𝑝, 𝑞〉))} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) |
49 | 17, 48 | bitrd 278 |
. . 3
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V) → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) |
50 | 49 | 3expia 1120 |
. 2
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑃 ∈ V → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉))))) |
51 | 3, 8, 50 | pm5.21ndd 381 |
1
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑃 Colinear 〈𝑄, 𝑅〉 ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn 〈𝑄, 𝑅〉 ∨ 𝑄 Btwn 〈𝑅, 𝑃〉 ∨ 𝑅 Btwn 〈𝑃, 𝑄〉)))) |