Metamath Proof Explorer

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 = x ∈ 𝒫 RR3 | 2 𝑜 ≼ x ∧ ∀ y ∈ x ∀ z ∈ x z ≠ y → ran ⁡ PtDf y z = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cline3 class line3
1 vx setvar x
2 crr3c class RR3
3 2 cpw class 𝒫 RR3
4 c2o class 2 𝑜
5 cdom class ≼
6 1 cv setvar x
7 4 6 5 wbr wff 2 𝑜 ≼ x
8 vy setvar y
9 vz setvar z
10 9 cv setvar z
11 8 cv setvar y
12 10 11 wne wff z ≠ y
13 11 10 cptdfc class PtDf y z
14 13 crn class ran ⁡ PtDf y z
15 14 6 wceq wff ran ⁡ PtDf y z = x
16 12 15 wi wff z ≠ y → ran ⁡ PtDf y z = x
17 16 9 6 wral wff ∀ z ∈ x z ≠ y → ran ⁡ PtDf y z = x
18 17 8 6 wral wff ∀ y ∈ x ∀ z ∈ x z ≠ y → ran ⁡ PtDf y z = x
19 7 18 wa wff 2 𝑜 ≼ x ∧ ∀ y ∈ x ∀ z ∈ x z ≠ y → ran ⁡ PtDf y z = x
20 19 1 3 crab class x ∈ 𝒫 RR3 | 2 𝑜 ≼ x ∧ ∀ y ∈ x ∀ z ∈ x z ≠ y → ran ⁡ PtDf y z = x
21 0 20 wceq wff line3 = x ∈ 𝒫 RR3 | 2 𝑜 ≼ x ∧ ∀ y ∈ x ∀ z ∈ x z ≠ y → ran ⁡ PtDf y z = x