Definition df-line2 33598

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 33595	. 2 class Line
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1532	. . . . . . 7 class 𝑎
4		vn	. . . . . . . . 9 setvar 𝑛
5	4	cv 1532	. . . . . . . 8 class 𝑛
6		cee 26673	. . . . . . . 8 class 𝔼
7	5, 6	cfv 6354	. . . . . . 7 class (𝔼‘𝑛)
8	3, 7	wcel 2110	. . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . 8 setvar 𝑏
10	9	cv 1532	. . . . . . 7 class 𝑏
11	10, 7	wcel 2110	. . . . . 6 wff 𝑏 ∈ (𝔼‘𝑛)
12	3, 10	wne 3016	. . . . . 6 wff 𝑎 ≠ 𝑏
13	8, 11, 12	w3a 1083	. . . . 5 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏)
14		vl	. . . . . . 7 setvar 𝑙
15	14	cv 1532	. . . . . 6 class 𝑙
16	3, 10	cop 4572	. . . . . . 7 class ⟨𝑎, 𝑏⟩
17		ccolin 33498	. . . . . . . 8 class Colinear
18	17	ccnv 5553	. . . . . . 7 class ◡ Colinear
19	16, 18	cec 8286	. . . . . 6 class [⟨𝑎, 𝑏⟩]◡ Colinear
20	15, 19	wceq 1533	. . . . 5 wff 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear
21	13, 20	wa 398	. . . 4 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
22		cn 11637	. . . 4 class ℕ
23	21, 4, 22	wrex 3139	. . 3 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
24	23, 2, 9, 14	coprab 7156	. 2 class {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}
25	1, 24	wceq 1533	1 wff Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}

This definition is referenced by:  funline  33603  linedegen  33604  fvline  33605  ellines  33613