Definition df-line3 44497

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.)

Assertion

Ref	Expression
df-line3	⊢ line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-line3

Step	Hyp	Ref	Expression
1		cline3 44481	. 2 class line3
2		c2o 8500	. . . . 5 class 2o
3		vx	. . . . . 6 setvar 𝑥
4	3	cv 1539	. . . . 5 class 𝑥
5		cdom 8983	. . . . 5 class ≼
6	2, 4, 5	wbr 5143	. . . 4 wff 2o ≼ 𝑥
7		vz	. . . . . . . . 9 setvar 𝑧
8	7	cv 1539	. . . . . . . 8 class 𝑧
9		vy	. . . . . . . . 9 setvar 𝑦
10	9	cv 1539	. . . . . . . 8 class 𝑦
11	8, 10	wne 2940	. . . . . . 7 wff 𝑧 ≠ 𝑦
12	10, 8	cptdfc 44479	. . . . . . . . 9 class PtDf(𝑦, 𝑧)
13	12	crn 5686	. . . . . . . 8 class ran PtDf(𝑦, 𝑧)
14	13, 4	wceq 1540	. . . . . . 7 wff ran PtDf(𝑦, 𝑧) = 𝑥
15	11, 14	wi 4	. . . . . 6 wff (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥)
16	15, 7, 4	wral 3061	. . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥)
17	16, 9, 4	wral 3061	. . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥)
18	6, 17	wa 395	. . 3 wff (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))
19		crr3c 44480	. . . 4 class RR3
20	19	cpw 4600	. . 3 class 𝒫 RR3
21	18, 3, 20	crab 3436	. 2 class {𝑥 ∈ 𝒫 RR3 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}
22	1, 21	wceq 1540	1 wff line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}

This definition is referenced by: (None)