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⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land 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 \in 𝔼 (n)$
11	2	cv	$setvar b$
12	11 9	wcel	$wff b \in 𝔼 (n)$
13	6 11	wne	$wff a \neq b$
14	10 12 13	w3a	$wff (a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq 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 \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})$
22	21 4 5	wrex	$wff \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})$
23	22 1 2 3	coprab	$class \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
24	0 23	wceq	$wff Line = \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$

Metamath Proof Explorer

Definition df-line2

Detailed syntax breakdown