Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . 5
⊢
[〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear |
2 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁)) |
3 | 2 | eleq2d 2818 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐴 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑁))) |
4 | 2 | eleq2d 2818 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐵 ∈ (𝔼‘𝑛) ↔ 𝐵 ∈ (𝔼‘𝑁))) |
5 | 3, 4 | 3anbi12d 1438 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵))) |
6 | 5 | anbi1d 633 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
7 | 6 | rspcev 3526 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) → ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) |
8 | 1, 7 | mpanr2 704 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) |
9 | | simpr1 1195 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ (𝔼‘𝑁)) |
10 | | simpr2 1196 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ (𝔼‘𝑁)) |
11 | | colinearex 34000 |
. . . . . . . 8
⊢ Colinear
∈ V |
12 | 11 | cnvex 7656 |
. . . . . . 7
⊢ ◡ Colinear ∈ V |
13 | | ecexg 8324 |
. . . . . . 7
⊢ (◡ Colinear ∈ V → [〈𝐴, 𝐵〉]◡ Colinear ∈ V) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
⊢
[〈𝐴, 𝐵〉]◡ Colinear ∈ V |
15 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑎 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛))) |
16 | | neeq1 2996 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝑏)) |
17 | 15, 16 | 3anbi13d 1439 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ↔ (𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏))) |
18 | | opeq1 4759 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
19 | 18 | eceq1d 8359 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → [〈𝑎, 𝑏〉]◡ Colinear = [〈𝐴, 𝑏〉]◡ Colinear ) |
20 | 19 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑙 = [〈𝑎, 𝑏〉]◡ Colinear ↔ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear )) |
21 | 17, 20 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ))) |
22 | 21 | rexbidv 3207 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ))) |
23 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝔼‘𝑛) ↔ 𝐵 ∈ (𝔼‘𝑛))) |
24 | | neeq2 2997 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝐴 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵)) |
25 | 23, 24 | 3anbi23d 1440 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ↔ (𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵))) |
26 | | opeq2 4761 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) |
27 | 26 | eceq1d 8359 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → [〈𝐴, 𝑏〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ) |
28 | 27 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ↔ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear )) |
29 | 25, 28 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ))) |
30 | 29 | rexbidv 3207 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ))) |
31 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear → (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ↔ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) |
32 | 31 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear → (((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
33 | 32 | rexbidv 3207 |
. . . . . . 7
⊢ (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear → (∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
34 | 22, 30, 33 | eloprabg 7276 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ [〈𝐴, 𝐵〉]◡ Colinear ∈ V) →
(〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
35 | 14, 34 | mp3an3 1451 |
. . . . 5
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
36 | 9, 10, 35 | syl2anc 587 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
37 | 8, 36 | mpbird 260 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → 〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )}) |
38 | | df-ov 7173 |
. . . 4
⊢ (𝐴Line𝐵) = (Line‘〈𝐴, 𝐵〉) |
39 | | df-br 5031 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear ↔ 〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈
Line) |
40 | | df-line2 34077 |
. . . . . . 7
⊢ Line =
{〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} |
41 | 40 | eleq2i 2824 |
. . . . . 6
⊢
(〈〈𝐴,
𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ Line ↔
〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )}) |
42 | 39, 41 | bitri 278 |
. . . . 5
⊢
(〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear ↔ 〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )}) |
43 | | funline 34082 |
. . . . . 6
⊢ Fun
Line |
44 | | funbrfv 6720 |
. . . . . 6
⊢ (Fun Line
→ (〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear → (Line‘〈𝐴, 𝐵〉) = [〈𝐴, 𝐵〉]◡ Colinear )) |
45 | 43, 44 | ax-mp 5 |
. . . . 5
⊢
(〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear → (Line‘〈𝐴, 𝐵〉) = [〈𝐴, 𝐵〉]◡ Colinear ) |
46 | 42, 45 | sylbir 238 |
. . . 4
⊢
(〈〈𝐴,
𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} → (Line‘〈𝐴, 𝐵〉) = [〈𝐴, 𝐵〉]◡ Colinear ) |
47 | 38, 46 | syl5eq 2785 |
. . 3
⊢
(〈〈𝐴,
𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} → (𝐴Line𝐵) = [〈𝐴, 𝐵〉]◡ Colinear ) |
48 | 37, 47 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = [〈𝐴, 𝐵〉]◡ Colinear ) |
49 | | opex 5322 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
50 | | dfec2 8323 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ∈ V →
[〈𝐴, 𝐵〉]◡ Colinear = {𝑥 ∣ 〈𝐴, 𝐵〉◡ Colinear 𝑥}) |
51 | 49, 50 | ax-mp 5 |
. . 3
⊢
[〈𝐴, 𝐵〉]◡ Colinear = {𝑥 ∣ 〈𝐴, 𝐵〉◡ Colinear 𝑥} |
52 | | vex 3402 |
. . . . 5
⊢ 𝑥 ∈ V |
53 | 49, 52 | brcnv 5725 |
. . . 4
⊢
(〈𝐴, 𝐵〉◡ Colinear 𝑥 ↔ 𝑥 Colinear 〈𝐴, 𝐵〉) |
54 | 53 | abbii 2803 |
. . 3
⊢ {𝑥 ∣ 〈𝐴, 𝐵〉◡ Colinear 𝑥} = {𝑥 ∣ 𝑥 Colinear 〈𝐴, 𝐵〉} |
55 | 51, 54 | eqtri 2761 |
. 2
⊢
[〈𝐴, 𝐵〉]◡ Colinear = {𝑥 ∣ 𝑥 Colinear 〈𝐴, 𝐵〉} |
56 | 48, 55 | eqtrdi 2789 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∣ 𝑥 Colinear 〈𝐴, 𝐵〉}) |