Users' Mathboxes Mathbox for Andrew Salmon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-line3 Unicode version

Definition df-line3 27786
Description: Define the set of all lines. A line is an infinite subset of  RR 3 that satisfies a  PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.)
Assertion
Ref Expression
df-line3  |-  line 3  =  { x  e.  ~P RR 3  |  ( 2o 
~<_  x  /\  A. y  e.  x  A. z  e.  x  ( z  =/=  y  ->  ran  PtDf ( y ,  z )  =  x ) ) }
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-line3
StepHypRef Expression
1 cline3 27770 . 2  class  line 3
2 c2o 6489 . . . . 5  class  2o
3 vx . . . . . 6  set  x
43cv 1631 . . . . 5  class  x
5 cdom 6877 . . . . 5  class  ~<_
62, 4, 5wbr 4039 . . . 4  wff  2o  ~<_  x
7 vz . . . . . . . . 9  set  z
87cv 1631 . . . . . . . 8  class  z
9 vy . . . . . . . . 9  set  y
109cv 1631 . . . . . . . 8  class  y
118, 10wne 2459 . . . . . . 7  wff  z  =/=  y
1210, 8cptdfc 27768 . . . . . . . . 9  class  PtDf (
y ,  z )
1312crn 4706 . . . . . . . 8  class  ran  PtDf ( y ,  z )
1413, 4wceq 1632 . . . . . . 7  wff  ran  PtDf ( y ,  z )  =  x
1511, 14wi 4 . . . . . 6  wff  ( z  =/=  y  ->  ran  PtDf ( y ,  z )  =  x )
1615, 7, 4wral 2556 . . . . 5  wff  A. z  e.  x  ( z  =/=  y  ->  ran  PtDf ( y ,  z )  =  x )
1716, 9, 4wral 2556 . . . 4  wff  A. y  e.  x  A. z  e.  x  ( z  =/=  y  ->  ran  PtDf ( y ,  z )  =  x )
186, 17wa 358 . . 3  wff  ( 2o  ~<_  x  /\  A. y  e.  x  A. z  e.  x  ( z  =/=  y  ->  ran  PtDf ( y ,  z )  =  x ) )
19 crr3c 27769 . . . 4  class  RR 3
2019cpw 3638 . . 3  class  ~P RR 3
2118, 3, 20crab 2560 . 2  class  { x  e.  ~P RR 3  | 
( 2o  ~<_  x  /\  A. y  e.  x  A. z  e.  x  (
z  =/=  y  ->  ran  PtDf ( y ,  z )  =  x ) ) }
221, 21wceq 1632 1  wff  line 3  =  { x  e.  ~P RR 3  |  ( 2o 
~<_  x  /\  A. y  e.  x  A. z  e.  x  ( z  =/=  y  ->  ran  PtDf ( y ,  z )  =  x ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator