Definition df-line3

Description: Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012)

	Ref	Expression
Assertion	df-line3	$$⊢\mathrm{line3}=\left\{x\in 𝒫\mathrm{RR3}|\left(2_{𝑜}\preccurlyeq x\wedge \forall y\in x\forall z\in x\left(z\ne y\to \mathrm{ran}PtDf\left(y,z\right)=x\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cline3	$$class\mathrm{line3}$$
1		vx	$$setvarx$$
2		crr3c	$$class\mathrm{RR3}$$
3	2	cpw	$$class𝒫\mathrm{RR3}$$
4		c2o	$$class{2}_{𝑜}$$
5		cdom	$$class\preccurlyeq$$
6	1	cv	$$setvarx$$
7	4 6 5	wbr	$$wff{2}_{𝑜}\preccurlyeq x$$
8		vy	$$setvary$$
9		vz	$$setvarz$$
10	9	cv	$$setvarz$$
11	8	cv	$$setvary$$
12	10 11	wne	$$wffz\ne y$$
13	11 10	cptdfc	$$classPtDf\left(y,z\right)$$
14	13	crn	$$class\mathrm{ran}PtDf\left(y,z\right)$$
15	14 6	wceq	$$wff\mathrm{ran}PtDf\left(y,z\right)=x$$
16	12 15	wi	$$wff\left(z\ne y\to \mathrm{ran}PtDf\left(y,z\right)=x\right)$$
17	16 9 6	wral	$$wff\forall z\in x\left(z\ne y\to \mathrm{ran}PtDf\left(y,z\right)=x\right)$$
18	17 8 6	wral	$$wff\forall y\in x\forall z\in x\left(z\ne y\to \mathrm{ran}PtDf\left(y,z\right)=x\right)$$
19	7 18	wa	$$wff\left(2_{𝑜}\preccurlyeq x\wedge \forall y\in x\forall z\in x\left(z\ne y\to \mathrm{ran}PtDf\left(y,z\right)=x\right)\right)$$
20	19 1 3	crab	$$class\left\{x\in 𝒫\mathrm{RR3}|\left(2_{𝑜}\preccurlyeq x\wedge \forall y\in x\forall z\in x\left(z\ne y\to \mathrm{ran}PtDf\left(y,z\right)=x\right)\right)\right\}$$
21	0 20	wceq	$$wff\mathrm{line3}=\left\{x\in 𝒫\mathrm{RR3}|\left(2_{𝑜}\preccurlyeq x\wedge \forall y\in x\forall z\in x\left(z\ne y\to \mathrm{ran}PtDf\left(y,z\right)=x\right)\right)\right\}$$