Metamath Proof Explorer

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 = a b l | ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ a ≠ b ∧ l = a b Colinear -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cline2 class Line
1 va setvar a
2 vb setvar b
3 vl setvar l
4 vn setvar n
5 cn class ℕ
6 1 cv setvar a
7 cee class 𝔼
8 4 cv setvar n
9 8 7 cfv class 𝔼 ⁡ n
10 6 9 wcel wff a ∈ 𝔼 ⁡ n
11 2 cv setvar b
12 11 9 wcel wff b ∈ 𝔼 ⁡ n
13 6 11 wne wff a ≠ b
14 10 12 13 w3a wff a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ a ≠ b
15 3 cv setvar l
16 6 11 cop class a b
17 ccolin class Colinear
18 17 ccnv class Colinear -1
19 16 18 cec class a b Colinear -1
20 15 19 wceq wff l = a b Colinear -1
21 14 20 wa wff a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ a ≠ b ∧ l = a b Colinear -1
22 21 4 5 wrex wff ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ a ≠ b ∧ l = a b Colinear -1
23 22 1 2 3 coprab class a b l | ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ a ≠ b ∧ l = a b Colinear -1
24 0 23 wceq wff Line = a b l | ∃ n ∈ ℕ a ∈ 𝔼 ⁡ n ∧ b ∈ 𝔼 ⁡ n ∧ a ≠ b ∧ l = a b Colinear -1