Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
[〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear |
2 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁)) |
3 | 2 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐴 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑁))) |
4 | 2 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐵 ∈ (𝔼‘𝑛) ↔ 𝐵 ∈ (𝔼‘𝑁))) |
5 | 3, 4 | 3anbi12d 1392 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ↔ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵))) |
6 | 5 | anbi1d 737 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
7 | 6 | rspcev 3282 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) → ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) |
8 | 1, 7 | mpanr2 716 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) |
9 | | simpr1 1060 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → 𝐴 ∈ (𝔼‘𝑁)) |
10 | | simpr2 1061 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → 𝐵 ∈ (𝔼‘𝑁)) |
11 | | colinearex 31337 |
. . . . . . . 8
⊢ Colinear
∈ V |
12 | 11 | cnvex 7006 |
. . . . . . 7
⊢ ◡ Colinear ∈ V |
13 | | ecexg 7633 |
. . . . . . 7
⊢ (◡ Colinear ∈ V → [〈𝐴, 𝐵〉]◡ Colinear ∈ V) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
⊢
[〈𝐴, 𝐵〉]◡ Colinear ∈ V |
15 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑎 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛))) |
16 | | neeq1 2844 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝑏)) |
17 | 15, 16 | 3anbi13d 1393 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ↔ (𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏))) |
18 | | opeq1 4340 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
19 | 18 | eceq1d 7670 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → [〈𝑎, 𝑏〉]◡ Colinear = [〈𝐴, 𝑏〉]◡ Colinear ) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑙 = [〈𝑎, 𝑏〉]◡ Colinear ↔ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear )) |
21 | 17, 20 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ))) |
22 | 21 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ))) |
23 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝔼‘𝑛) ↔ 𝐵 ∈ (𝔼‘𝑛))) |
24 | | neeq2 2845 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (𝐴 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵)) |
25 | 23, 24 | 3anbi23d 1394 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ↔ (𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵))) |
26 | | opeq2 4341 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) |
27 | 26 | eceq1d 7670 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → [〈𝐴, 𝑏〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ) |
28 | 27 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ↔ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear )) |
29 | 25, 28 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ))) |
30 | 29 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑏) ∧ 𝑙 = [〈𝐴, 𝑏〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ))) |
31 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear → (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ↔ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear )) |
32 | 31 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear → (((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
33 | 32 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑙 = [〈𝐴, 𝐵〉]◡ Colinear → (∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ 𝑙 = [〈𝐴, 𝐵〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
34 | 22, 30, 33 | eloprabg 6646 |
. . . . . 6
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ [〈𝐴, 𝐵〉]◡ Colinear ∈ V) →
(〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
35 | 14, 34 | mp3an3 1405 |
. . . . 5
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
36 | 9, 10, 35 | syl2anc 691 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐵 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐵) ∧ [〈𝐴, 𝐵〉]◡ Colinear = [〈𝐴, 𝐵〉]◡ Colinear ))) |
37 | 8, 36 | mpbird 246 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → 〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )}) |
38 | | df-ov 6552 |
. . . 4
⊢ (𝐴Line𝐵) = (Line‘〈𝐴, 𝐵〉) |
39 | | df-br 4584 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear ↔ 〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈
Line) |
40 | | df-line2 31414 |
. . . . . . 7
⊢ Line =
{〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} |
41 | 40 | eleq2i 2680 |
. . . . . 6
⊢
(〈〈𝐴,
𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ Line ↔
〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )}) |
42 | 39, 41 | bitri 263 |
. . . . 5
⊢
(〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear ↔ 〈〈𝐴, 𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )}) |
43 | | funline 31419 |
. . . . . 6
⊢ Fun
Line |
44 | | funbrfv 6144 |
. . . . . 6
⊢ (Fun Line
→ (〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear → (Line‘〈𝐴, 𝐵〉) = [〈𝐴, 𝐵〉]◡ Colinear )) |
45 | 43, 44 | ax-mp 5 |
. . . . 5
⊢
(〈𝐴, 𝐵〉Line[〈𝐴, 𝐵〉]◡ Colinear → (Line‘〈𝐴, 𝐵〉) = [〈𝐴, 𝐵〉]◡ Colinear ) |
46 | 42, 45 | sylbir 224 |
. . . 4
⊢
(〈〈𝐴,
𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} → (Line‘〈𝐴, 𝐵〉) = [〈𝐴, 𝐵〉]◡ Colinear ) |
47 | 38, 46 | syl5eq 2656 |
. . 3
⊢
(〈〈𝐴,
𝐵〉, [〈𝐴, 𝐵〉]◡ Colinear 〉 ∈ {〈〈𝑎, 𝑏〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [〈𝑎, 𝑏〉]◡ Colinear )} → (𝐴Line𝐵) = [〈𝐴, 𝐵〉]◡ Colinear ) |
48 | 37, 47 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = [〈𝐴, 𝐵〉]◡ Colinear ) |
49 | | opex 4859 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
50 | | dfec2 7632 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ∈ V →
[〈𝐴, 𝐵〉]◡ Colinear = {𝑥 ∣ 〈𝐴, 𝐵〉◡ Colinear 𝑥}) |
51 | 49, 50 | ax-mp 5 |
. . 3
⊢
[〈𝐴, 𝐵〉]◡ Colinear = {𝑥 ∣ 〈𝐴, 𝐵〉◡ Colinear 𝑥} |
52 | | vex 3176 |
. . . . 5
⊢ 𝑥 ∈ V |
53 | 49, 52 | brcnv 5227 |
. . . 4
⊢
(〈𝐴, 𝐵〉◡ Colinear 𝑥 ↔ 𝑥 Colinear 〈𝐴, 𝐵〉) |
54 | 53 | abbii 2726 |
. . 3
⊢ {𝑥 ∣ 〈𝐴, 𝐵〉◡ Colinear 𝑥} = {𝑥 ∣ 𝑥 Colinear 〈𝐴, 𝐵〉} |
55 | 51, 54 | eqtri 2632 |
. 2
⊢
[〈𝐴, 𝐵〉]◡ Colinear = {𝑥 ∣ 𝑥 Colinear 〈𝐴, 𝐵〉} |
56 | 48, 55 | syl6eq 2660 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∣ 𝑥 Colinear 〈𝐴, 𝐵〉}) |