Definition df-line2 31414

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 31411	. 2 class Line
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1474	. . . . . . 7 class 𝑎
4		vn	. . . . . . . . 9 setvar 𝑛
5	4	cv 1474	. . . . . . . 8 class 𝑛
6		cee 25568	. . . . . . . 8 class 𝔼
7	5, 6	cfv 5804	. . . . . . 7 class (𝔼‘𝑛)
8	3, 7	wcel 1977	. . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . 8 setvar 𝑏
10	9	cv 1474	. . . . . . 7 class 𝑏
11	10, 7	wcel 1977	. . . . . 6 wff 𝑏 ∈ (𝔼‘𝑛)
12	3, 10	wne 2780	. . . . . 6 wff 𝑎 ≠ 𝑏
13	8, 11, 12	w3a 1031	. . . . 5 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏)
14		vl	. . . . . . 7 setvar 𝑙
15	14	cv 1474	. . . . . 6 class 𝑙
16	3, 10	cop 4131	. . . . . . 7 class ⟨𝑎, 𝑏⟩
17		ccolin 31314	. . . . . . . 8 class Colinear
18	17	ccnv 5037	. . . . . . 7 class ◡ Colinear
19	16, 18	cec 7627	. . . . . 6 class [⟨𝑎, 𝑏⟩]◡ Colinear
20	15, 19	wceq 1475	. . . . 5 wff 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear
21	13, 20	wa 383	. . . 4 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
22		cn 10897	. . . 4 class ℕ
23	21, 4, 22	wrex 2897	. . 3 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
24	23, 2, 9, 14	coprab 6550	. 2 class {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}
25	1, 24	wceq 1475	1 wff Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}

This definition is referenced by:  funline  31419  linedegen  31420  fvline  31421  ellines  31429