Definition df-line2 36994

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 36991	. 2 class Line
2		va	. . . . . . . 8 setvar 𝑎
3	2	cv 1568	. . . . . . 7 class 𝑎
4		vn	. . . . . . . . 9 setvar 𝑛
5	4	cv 1568	. . . . . . . 8 class 𝑛
6		cee 29470	. . . . . . . 8 class 𝔼
7	5, 6	cfv 6538	. . . . . . 7 class (𝔼‘𝑛)
8	3, 7	wcel 2144	. . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
9		vb	. . . . . . . 8 setvar 𝑏
10	9	cv 1568	. . . . . . 7 class 𝑏
11	10, 7	wcel 2144	. . . . . 6 wff 𝑏 ∈ (𝔼‘𝑛)
12	3, 10	wne 2955	. . . . . 6 wff 𝑎 ≠ 𝑏
13	8, 11, 12	w3a 1103	. . . . 5 wff (𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏)
14		vl	. . . . . . 7 setvar 𝑙
15	14	cv 1568	. . . . . 6 class 𝑙
16	3, 10	cop 4834	. . . . . . 7 class ⟨𝑎, 𝑏⟩
17		ccolin 36894	. . . . . . . 8 class Colinear
18	17	ccnv 5649	. . . . . . 7 class ◡ Colinear
19	16, 18	cec 8718	. . . . . 6 class [⟨𝑎, 𝑏⟩]◡ Colinear
20	15, 19	wceq 1569	. . . . 5 wff 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear
21	13, 20	wa 401	. . . 4 wff ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
22		cn 12338	. . . 4 class ℕ
23	21, 4, 22	wrex 3086	. . 3 wff ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )
24	23, 2, 9, 14	coprab 7421	. 2 class {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}
25	1, 24	wceq 1569	1 wff Line = {⟨⟨𝑎, 𝑏⟩, 𝑙⟩ ∣ ∃𝑛 ∈ ℕ ((𝑎 ∈ (𝔼‘𝑛) ∧ 𝑏 ∈ (𝔼‘𝑛) ∧ 𝑎 ≠ 𝑏) ∧ 𝑙 = [⟨𝑎, 𝑏⟩]◡ Colinear )}

This definition is used by:  funline  36999  linedegen  37000  fvline  37001  ellines  37009