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

Definition df-crcl 25531
Description: Definition of a circle (degenerated or not). Definition 5 of [AitkenNG] p. 4. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-crcl  |- Circle  =  ( g  e. Ibcg  |->  ( x  e.  (PPoints `  g
) ,  y  e.  (PPoints `  g )  |->  { u  e.  (PPoints `  g )  |  ( x ( seg `  g
) u ) (segc `  g ) ( x ( seg `  g
) y ) } ) )
Distinct variable group:    x, g, y, u

Detailed syntax breakdown of Definition df-crcl
StepHypRef Expression
1 ccircle 25530 . 2  class Circle
2 vg . . 3  set  g
3 cibcg 25513 . . 3  class Ibcg
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1618 . . . . 5  class  g
7 cpoints 25388 . . . . 5  class PPoints
86, 7cfv 4638 . . . 4  class  (PPoints `  g
)
94cv 1618 . . . . . . 7  class  x
10 vu . . . . . . . 8  set  u
1110cv 1618 . . . . . . 7  class  u
12 cseg 25462 . . . . . . . 8  class  seg
136, 12cfv 4638 . . . . . . 7  class  ( seg `  g )
149, 11, 13co 5757 . . . . . 6  class  ( x ( seg `  g
) u )
155cv 1618 . . . . . . 7  class  y
169, 15, 13co 5757 . . . . . 6  class  ( x ( seg `  g
) y )
17 csegc 25512 . . . . . . 7  class segc
186, 17cfv 4638 . . . . . 6  class  (segc `  g )
1914, 16, 18wbr 3963 . . . . 5  wff  ( x ( seg `  g
) u ) (segc `  g ) ( x ( seg `  g
) y )
2019, 10, 8crab 2519 . . . 4  class  { u  e.  (PPoints `  g )  |  ( x ( seg `  g ) u ) (segc `  g ) ( x ( seg `  g
) y ) }
214, 5, 8, 8, 20cmpt2 5759 . . 3  class  ( x  e.  (PPoints `  g
) ,  y  e.  (PPoints `  g )  |->  { u  e.  (PPoints `  g )  |  ( x ( seg `  g
) u ) (segc `  g ) ( x ( seg `  g
) y ) } )
222, 3, 21cmpt 4017 . 2  class  ( g  e. Ibcg  |->  ( x  e.  (PPoints `  g ) ,  y  e.  (PPoints `  g )  |->  { u  e.  (PPoints `  g )  |  ( x ( seg `  g ) u ) (segc `  g ) ( x ( seg `  g
) y ) } ) )
231, 22wceq 1619 1  wff Circle  =  ( g  e. Ibcg  |->  ( x  e.  (PPoints `  g
) ,  y  e.  (PPoints `  g )  |->  { u  e.  (PPoints `  g )  |  ( x ( seg `  g
) u ) (segc `  g ) ( x ( seg `  g
) y ) } ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator