Definition df-line2

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cline2	⊢ Line
1		va	⊢ 𝑎
2		vb	⊢ 𝑏
3		vl	⊢ 𝑙
4		vn	⊢ 𝑛
5		cn	⊢ ℕ
6	1	cv	⊢ 𝑎
7		cee	⊢ 𝔼
8	4	cv	⊢ 𝑛
9	8 7	cfv	⊢ ( 𝔼 ‘ 𝑛 )
10	6 9	wcel	⊢ 𝑎 ∈ ( 𝔼 ‘ 𝑛 )
11	2	cv	⊢ 𝑏
12	11 9	wcel	⊢ 𝑏 ∈ ( 𝔼 ‘ 𝑛 )
13	6 11	wne	⊢ 𝑎 ≠ 𝑏
14	10 12 13	w3a	⊢ ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 )
15	3	cv	⊢ 𝑙
16	6 11	cop	⊢ ⟨ 𝑎 , 𝑏 ⟩
17		ccolin	⊢ Colinear
18	17	ccnv	⊢ ◡ Colinear
19	16 18	cec	⊢ [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear
20	15 19	wceq	⊢ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear
21	14 20	wa	⊢ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear )
22	21 4 5	wrex	⊢ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear )
23	22 1 2 3	coprab	⊢ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) }
24	0 23	wceq	⊢ Line = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) }