Definition df-line2 34439

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 34436	. 2 class Line
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1538	. . . . . . 7 class 𝑎
4		vn	. . . . . . . . 9 setvar 𝑛
5	4	cv 1538	. . . . . . . 8 class 𝑛
6		cee 27256	. . . . . . . 8 class 𝔼
7	5, 6	cfv 6433	. . . . . . 7 class (𝔼‘𝑛)
8	3, 7	wcel 2106	. . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . 8 setvar 𝑏
10	9	cv 1538	. . . . . . 7 class 𝑏
11	10, 7	wcel 2106	. . . . . 6 wff 𝑏 ∈ (𝔼‘𝑛)
12	3, 10	wne 2943	. . . . . 6 wff 𝑎 ≠ 𝑏
13	8, 11, 12	w3a 1086	. . . . 5 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏)
14		vl	. . . . . . 7 setvar 𝑙
15	14	cv 1538	. . . . . 6 class 𝑙
16	3, 10	cop 4567	. . . . . . 7 class ⟨𝑎, 𝑏⟩
17		ccolin 34339	. . . . . . . 8 class Colinear
18	17	ccnv 5588	. . . . . . 7 class ◡ Colinear
19	16, 18	cec 8496	. . . . . 6 class [⟨𝑎, 𝑏⟩]◡ Colinear
20	15, 19	wceq 1539	. . . . 5 wff 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear
21	13, 20	wa 396	. . . 4 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
22		cn 11973	. . . 4 class ℕ
23	21, 4, 22	wrex 3065	. . 3 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
24	23, 2, 9, 14	coprab 7276	. 2 class {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}
25	1, 24	wceq 1539	1 wff Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}

This definition is referenced by:  funline  34444  linedegen  34445  fvline  34446  ellines  34454