Definition df-line3 42096

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 42080	. 2 class line3
2		c2o 8291	. . . . 5 class 2o
3		vx	. . . . . 6 setvar 𝑥
4	3	cv 1538	. . . . 5 class 𝑥
5		cdom 8731	. . . . 5 class ≼
6	2, 4, 5	wbr 5074	. . . 4 wff 2o ≼ 𝑥
7		vz	. . . . . . . . 9 setvar 𝑧
8	7	cv 1538	. . . . . . . 8 class 𝑧
9		vy	. . . . . . . . 9 setvar 𝑦
10	9	cv 1538	. . . . . . . 8 class 𝑦
11	8, 10	wne 2943	. . . . . . 7 wff 𝑧 ≠ 𝑦
12	10, 8	cptdfc 42078	. . . . . . . . 9 class PtDf(𝑦, 𝑧)
13	12	crn 5590	. . . . . . . 8 class ran PtDf(𝑦, 𝑧)
14	13, 4	wceq 1539	. . . . . . 7 wff ran PtDf(𝑦, 𝑧) = 𝑥
15	11, 14	wi 4	. . . . . 6 wff (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥)
16	15, 7, 4	wral 3064	. . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥)
17	16, 9, 4	wral 3064	. . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥)
18	6, 17	wa 396	. . 3 wff (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))
19		crr3c 42079	. . . 4 class RR3
20	19	cpw 4533	. . 3 class 𝒫 RR3
21	18, 3, 20	crab 3068	. 2 class {𝑥 ∈ 𝒫 RR3 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}
22	1, 21	wceq 1539	1 wff line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}

This definition is referenced by: (None)