Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-li Unicode version

Definition df-li 26088
Description: Definition of the line xy. It also defines a degenerate line. Definition 4 of [AitkenIBG] p. 2. (For my private use only. Don't use.) (Contributed by FL, 2-Apr-2016.)
Assertion
Ref Expression
df-li  |-  line  =  ( f  e. Ig  |->  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( iota_ l  e.  (PLines `  f
) ( x  e.  l  /\  y  e.  l ) ) ,  { x } ) ) )
Distinct variable group:    x, f, y, l

Detailed syntax breakdown of Definition df-li
StepHypRef Expression
1 cline 26087 . 2  class  line
2 vf . . 3  set  f
3 cig 26071 . . 3  class Ig
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1624 . . . . 5  class  f
7 cpoints 26067 . . . . 5  class PPoints
86, 7cfv 5257 . . . 4  class  (PPoints `  f
)
94cv 1624 . . . . . 6  class  x
105cv 1624 . . . . . 6  class  y
119, 10wne 2448 . . . . 5  wff  x  =/=  y
12 vl . . . . . . . 8  set  l
134, 12wel 1687 . . . . . . 7  wff  x  e.  l
145, 12wel 1687 . . . . . . 7  wff  y  e.  l
1513, 14wa 358 . . . . . 6  wff  ( x  e.  l  /\  y  e.  l )
16 cplines 26069 . . . . . . 7  class PLines
176, 16cfv 5257 . . . . . 6  class  (PLines `  f )
1815, 12, 17crio 6299 . . . . 5  class  ( iota_ l  e.  (PLines `  f
) ( x  e.  l  /\  y  e.  l ) )
199csn 3642 . . . . 5  class  { x }
2011, 18, 19cif 3567 . . . 4  class  if ( x  =/=  y ,  ( iota_ l  e.  (PLines `  f ) ( x  e.  l  /\  y  e.  l ) ) ,  { x } )
214, 5, 8, 8, 20cmpt2 5862 . . 3  class  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( iota_ l  e.  (PLines `  f
) ( x  e.  l  /\  y  e.  l ) ) ,  { x } ) )
222, 3, 21cmpt 4079 . 2  class  ( f  e. Ig  |->  ( x  e.  (PPoints `  f ) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( iota_ l  e.  (PLines `  f ) ( x  e.  l  /\  y  e.  l ) ) ,  { x } ) ) )
231, 22wceq 1625 1  wff  line  =  ( f  e. Ig  |->  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( iota_ l  e.  (PLines `  f
) ( x  e.  l  /\  y  e.  l ) ) ,  { x } ) ) )
Colors of variables: wff set class
This definition is referenced by:  linevala2  26089
  Copyright terms: Public domain W3C validator