Definition df-line2 32833

Description: Define the Line function. This function generates the line passing through the distinct points 𝑎 and 𝑏. Adapted from definition 6.14 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 25-Oct-2013.)

Assertion

Ref	Expression
df-line2	⊢ Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}

Distinct variable group:   𝑎,𝑏,𝑙,𝑛

Detailed syntax breakdown of Definition df-line2

Step	Hyp	Ref	Expression
1		cline2 32830	. 2 class Line
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1600	. . . . . . 7 class 𝑎
4		vn	. . . . . . . . 9 setvar 𝑛
5	4	cv 1600	. . . . . . . 8 class 𝑛
6		cee 26237	. . . . . . . 8 class 𝔼
7	5, 6	cfv 6135	. . . . . . 7 class (𝔼‘𝑛)
8	3, 7	wcel 2106	. . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . 8 setvar 𝑏
10	9	cv 1600	. . . . . . 7 class 𝑏
11	10, 7	wcel 2106	. . . . . 6 wff 𝑏 ∈ (𝔼‘𝑛)
12	3, 10	wne 2968	. . . . . 6 wff 𝑎 ≠ 𝑏
13	8, 11, 12	w3a 1071	. . . . 5 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏)
14		vl	. . . . . . 7 setvar 𝑙
15	14	cv 1600	. . . . . 6 class 𝑙
16	3, 10	cop 4403	. . . . . . 7 class ⟨𝑎, 𝑏⟩
17		ccolin 32733	. . . . . . . 8 class Colinear
18	17	ccnv 5354	. . . . . . 7 class ◡ Colinear
19	16, 18	cec 8024	. . . . . 6 class [⟨𝑎, 𝑏⟩]◡ Colinear
20	15, 19	wceq 1601	. . . . 5 wff 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear
21	13, 20	wa 386	. . . 4 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
22		cn 11374	. . . 4 class ℕ
23	21, 4, 22	wrex 3090	. . 3 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
24	23, 2, 9, 14	coprab 6923	. 2 class {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}
25	1, 24	wceq 1601	1 wff Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}

This definition is referenced by:  funline  32838  linedegen  32839  fvline  32840  ellines  32848