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	⊢ line3 = { 𝑥 ∈ 𝒫 RR3 ∣ ( 2o ≼ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ 𝑦 → ran PtDf ( 𝑦 , 𝑧 ) = 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cline3	⊢ line3
1		vx	⊢ 𝑥
2		crr3c	⊢ RR3
3	2	cpw	⊢ 𝒫 RR3
4		c2o	⊢ 2o
5		cdom	⊢ ≼
6	1	cv	⊢ 𝑥
7	4 6 5	wbr	⊢ 2o ≼ 𝑥
8		vy	⊢ 𝑦
9		vz	⊢ 𝑧
10	9	cv	⊢ 𝑧
11	8	cv	⊢ 𝑦
12	10 11	wne	⊢ 𝑧 ≠ 𝑦
13	11 10	cptdfc	⊢ PtDf ( 𝑦 , 𝑧 )
14	13	crn	⊢ ran PtDf ( 𝑦 , 𝑧 )
15	14 6	wceq	⊢ ran PtDf ( 𝑦 , 𝑧 ) = 𝑥
16	12 15	wi	⊢ ( 𝑧 ≠ 𝑦 → ran PtDf ( 𝑦 , 𝑧 ) = 𝑥 )
17	16 9 6	wral	⊢ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ 𝑦 → ran PtDf ( 𝑦 , 𝑧 ) = 𝑥 )
18	17 8 6	wral	⊢ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ 𝑦 → ran PtDf ( 𝑦 , 𝑧 ) = 𝑥 )
19	7 18	wa	⊢ ( 2o ≼ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ 𝑦 → ran PtDf ( 𝑦 , 𝑧 ) = 𝑥 ) )
20	19 1 3	crab	⊢ { 𝑥 ∈ 𝒫 RR3 ∣ ( 2o ≼ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ 𝑦 → ran PtDf ( 𝑦 , 𝑧 ) = 𝑥 ) ) }
21	0 20	wceq	⊢ line3 = { 𝑥 ∈ 𝒫 RR3 ∣ ( 2o ≼ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ 𝑦 → ran PtDf ( 𝑦 , 𝑧 ) = 𝑥 ) ) }