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 e. ~P RR3 | ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cline3 
 |-  line3
1 vx 
 |-  x
2 crr3c 
 |-  RR3
3 2 cpw 
 |-  ~P RR3
4 c2o 
 |-  2o
5 cdom 
 |-  ~<_
6 1 cv 
 |-  x
7 4 6 5 wbr 
 |-  2o ~<_ x
8 vy 
 |-  y
9 vz 
 |-  z
10 9 cv 
 |-  z
11 8 cv 
 |-  y
12 10 11 wne 
 |-  z =/= y
13 11 10 cptdfc 
 |-  PtDf ( y , z )
14 13 crn 
 |-  ran PtDf ( y , z )
15 14 6 wceq 
 |-  ran PtDf ( y , z ) = x
16 12 15 wi 
 |-  ( z =/= y -> ran PtDf ( y , z ) = x )
17 16 9 6 wral 
 |-  A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x )
18 17 8 6 wral 
 |-  A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x )
19 7 18 wa 
 |-  ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) )
20 19 1 3 crab 
 |-  { x e. ~P RR3 | ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) ) }
21 0 20 wceq 
 |-  line3 = { x e. ~P RR3 | ( 2o ~<_ x /\ A. y e. x A. z e. x ( z =/= y -> ran PtDf ( y , z ) = x ) ) }