| Step | Hyp | Ref
| Expression |
| 1 | | df-ov 7434 |
. 2
⊢ (𝐴Line𝐴) = (Line‘〈𝐴, 𝐴〉) |
| 2 | | neirr 2949 |
. . . . . . . . . . 11
⊢ ¬
𝐴 ≠ 𝐴 |
| 3 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴) → 𝐴 ≠ 𝐴) |
| 4 | 2, 3 | mto 197 |
. . . . . . . . . 10
⊢ ¬
(𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ≠ 𝐴) |
| 5 | 4 | intnanr 487 |
. . . . . . . . 9
⊢ ¬
((𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ) |
| 6 | 5 | a1i 11 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → ¬
((𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear )) |
| 7 | 6 | nrex 3074 |
. . . . . . 7
⊢ ¬
∃𝑛 ∈ ℕ
((𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ∈
(𝔼‘𝑛) ∧
𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ) |
| 8 | 7 | nex 1800 |
. . . . . 6
⊢ ¬
∃𝑙∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ) |
| 9 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛))) |
| 10 | | neeq1 3003 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦)) |
| 11 | 9, 10 | 3anbi13d 1440 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ↔ (𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦))) |
| 12 | | opeq1 4873 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) |
| 13 | 12 | eceq1d 8785 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → [〈𝑥, 𝑦〉]◡ Colinear = [〈𝐴, 𝑦〉]◡ Colinear ) |
| 14 | 13 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (𝑙 = [〈𝑥, 𝑦〉]◡ Colinear ↔ 𝑙 = [〈𝐴, 𝑦〉]◡ Colinear )) |
| 15 | 11, 14 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦) ∧ 𝑙 = [〈𝐴, 𝑦〉]◡ Colinear ))) |
| 16 | 15 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦) ∧ 𝑙 = [〈𝐴, 𝑦〉]◡ Colinear ))) |
| 17 | 16 | exbidv 1921 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear ) ↔ ∃𝑙∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦) ∧ 𝑙 = [〈𝐴, 𝑦〉]◡ Colinear ))) |
| 18 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑦 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛))) |
| 19 | | neeq2 3004 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐴)) |
| 20 | 18, 19 | 3anbi23d 1441 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦) ↔ (𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴))) |
| 21 | | opeq2 4874 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐴〉) |
| 22 | 21 | eceq1d 8785 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → [〈𝐴, 𝑦〉]◡ Colinear = [〈𝐴, 𝐴〉]◡ Colinear ) |
| 23 | 22 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (𝑙 = [〈𝐴, 𝑦〉]◡ Colinear ↔ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear )) |
| 24 | 20, 23 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦) ∧ 𝑙 = [〈𝐴, 𝑦〉]◡ Colinear ) ↔ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ))) |
| 25 | 24 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦) ∧ 𝑙 = [〈𝐴, 𝑦〉]◡ Colinear ) ↔ ∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ))) |
| 26 | 25 | exbidv 1921 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (∃𝑙∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝑦) ∧ 𝑙 = [〈𝐴, 𝑦〉]◡ Colinear ) ↔ ∃𝑙∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ))) |
| 27 | 17, 26 | opelopabg 5543 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → (〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} ↔ ∃𝑙∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ))) |
| 28 | 27 | anidms 566 |
. . . . . 6
⊢ (𝐴 ∈ V → (〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} ↔ ∃𝑙∃𝑛 ∈ ℕ ((𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝐴 ≠ 𝐴) ∧ 𝑙 = [〈𝐴, 𝐴〉]◡ Colinear ))) |
| 29 | 8, 28 | mtbiri 327 |
. . . . 5
⊢ (𝐴 ∈ V → ¬
〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )}) |
| 30 | | elopaelxp 5775 |
. . . . . . 7
⊢
(〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} → 〈𝐴, 𝐴〉 ∈ (V ×
V)) |
| 31 | | opelxp1 5727 |
. . . . . . 7
⊢
(〈𝐴, 𝐴〉 ∈ (V × V)
→ 𝐴 ∈
V) |
| 32 | 30, 31 | syl 17 |
. . . . . 6
⊢
(〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} → 𝐴 ∈ V) |
| 33 | 32 | con3i 154 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )}) |
| 34 | 29, 33 | pm2.61i 182 |
. . . 4
⊢ ¬
〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} |
| 35 | | df-line2 36138 |
. . . . . . 7
⊢ Line =
{〈〈𝑥, 𝑦〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} |
| 36 | 35 | dmeqi 5915 |
. . . . . 6
⊢ dom Line
= dom {〈〈𝑥, 𝑦〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} |
| 37 | | dmoprab 7536 |
. . . . . 6
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑙〉 ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} = {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} |
| 38 | 36, 37 | eqtri 2765 |
. . . . 5
⊢ dom Line
= {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )} |
| 39 | 38 | eleq2i 2833 |
. . . 4
⊢
(〈𝐴, 𝐴〉 ∈ dom Line ↔
〈𝐴, 𝐴〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑙∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛) ∧ 𝑥 ≠ 𝑦) ∧ 𝑙 = [〈𝑥, 𝑦〉]◡ Colinear )}) |
| 40 | 34, 39 | mtbir 323 |
. . 3
⊢ ¬
〈𝐴, 𝐴〉 ∈ dom Line |
| 41 | | ndmfv 6941 |
. . 3
⊢ (¬
〈𝐴, 𝐴〉 ∈ dom Line →
(Line‘〈𝐴, 𝐴〉) =
∅) |
| 42 | 40, 41 | ax-mp 5 |
. 2
⊢
(Line‘〈𝐴,
𝐴〉) =
∅ |
| 43 | 1, 42 | eqtri 2765 |
1
⊢ (𝐴Line𝐴) = ∅ |