MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-leg Structured version   Unicode version

Definition df-leg 23014
Description: Define the less-than relationship between geometric distance congruence classes. (Contributed by Thierry Arnoux, 21-Jun-2019.)
Assertion
Ref Expression
df-leg  |- ≤G  =  ( g  e.  _V  |->  {
<. e ,  f >.  |  [. ( Base `  g
)  /  p ]. [. ( dist `  g
)  /  d ]. [. (Itv `  g )  /  i ]. E. x  e.  p  E. y  e.  p  (
f  =  ( x d y )  /\  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x
d z ) ) ) } )
Distinct variable group:    e, d, f, g, i, p, x, y, z

Detailed syntax breakdown of Definition df-leg
StepHypRef Expression
1 cleg 23013 . 2  class ≤G
2 vg . . 3  setvar  g
3 cvv 2972 . . 3  class  _V
4 vf . . . . . . . . . . . 12  setvar  f
54cv 1368 . . . . . . . . . . 11  class  f
6 vx . . . . . . . . . . . . 13  setvar  x
76cv 1368 . . . . . . . . . . . 12  class  x
8 vy . . . . . . . . . . . . 13  setvar  y
98cv 1368 . . . . . . . . . . . 12  class  y
10 vd . . . . . . . . . . . . 13  setvar  d
1110cv 1368 . . . . . . . . . . . 12  class  d
127, 9, 11co 6091 . . . . . . . . . . 11  class  ( x d y )
135, 12wceq 1369 . . . . . . . . . 10  wff  f  =  ( x d y )
14 vz . . . . . . . . . . . . . 14  setvar  z
1514cv 1368 . . . . . . . . . . . . 13  class  z
16 vi . . . . . . . . . . . . . . 15  setvar  i
1716cv 1368 . . . . . . . . . . . . . 14  class  i
187, 9, 17co 6091 . . . . . . . . . . . . 13  class  ( x i y )
1915, 18wcel 1756 . . . . . . . . . . . 12  wff  z  e.  ( x i y )
20 ve . . . . . . . . . . . . . 14  setvar  e
2120cv 1368 . . . . . . . . . . . . 13  class  e
227, 15, 11co 6091 . . . . . . . . . . . . 13  class  ( x d z )
2321, 22wceq 1369 . . . . . . . . . . . 12  wff  e  =  ( x d z )
2419, 23wa 369 . . . . . . . . . . 11  wff  ( z  e.  ( x i y )  /\  e  =  ( x d z ) )
25 vp . . . . . . . . . . . 12  setvar  p
2625cv 1368 . . . . . . . . . . 11  class  p
2724, 14, 26wrex 2716 . . . . . . . . . 10  wff  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x d z ) )
2813, 27wa 369 . . . . . . . . 9  wff  ( f  =  ( x d y )  /\  E. z  e.  p  (
z  e.  ( x i y )  /\  e  =  ( x
d z ) ) )
2928, 8, 26wrex 2716 . . . . . . . 8  wff  E. y  e.  p  ( f  =  ( x d y )  /\  E. z  e.  p  (
z  e.  ( x i y )  /\  e  =  ( x
d z ) ) )
3029, 6, 26wrex 2716 . . . . . . 7  wff  E. x  e.  p  E. y  e.  p  ( f  =  ( x d y )  /\  E. z  e.  p  (
z  e.  ( x i y )  /\  e  =  ( x
d z ) ) )
312cv 1368 . . . . . . . 8  class  g
32 citv 22897 . . . . . . . 8  class Itv
3331, 32cfv 5418 . . . . . . 7  class  (Itv `  g )
3430, 16, 33wsbc 3186 . . . . . 6  wff  [. (Itv `  g )  /  i ]. E. x  e.  p  E. y  e.  p  ( f  =  ( x d y )  /\  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x d z ) ) )
35 cds 14247 . . . . . . 7  class  dist
3631, 35cfv 5418 . . . . . 6  class  ( dist `  g )
3734, 10, 36wsbc 3186 . . . . 5  wff  [. ( dist `  g )  / 
d ]. [. (Itv `  g )  /  i ]. E. x  e.  p  E. y  e.  p  ( f  =  ( x d y )  /\  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x d z ) ) )
38 cbs 14174 . . . . . 6  class  Base
3931, 38cfv 5418 . . . . 5  class  ( Base `  g )
4037, 25, 39wsbc 3186 . . . 4  wff  [. ( Base `  g )  /  p ]. [. ( dist `  g )  /  d ]. [. (Itv `  g
)  /  i ]. E. x  e.  p  E. y  e.  p  ( f  =  ( x d y )  /\  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x d z ) ) )
4140, 20, 4copab 4349 . . 3  class  { <. e ,  f >.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g )  / 
d ]. [. (Itv `  g )  /  i ]. E. x  e.  p  E. y  e.  p  ( f  =  ( x d y )  /\  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x d z ) ) ) }
422, 3, 41cmpt 4350 . 2  class  ( g  e.  _V  |->  { <. e ,  f >.  |  [. ( Base `  g )  /  p ]. [. ( dist `  g )  / 
d ]. [. (Itv `  g )  /  i ]. E. x  e.  p  E. y  e.  p  ( f  =  ( x d y )  /\  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x d z ) ) ) } )
431, 42wceq 1369 1  wff ≤G  =  ( g  e.  _V  |->  {
<. e ,  f >.  |  [. ( Base `  g
)  /  p ]. [. ( dist `  g
)  /  d ]. [. (Itv `  g )  /  i ]. E. x  e.  p  E. y  e.  p  (
f  =  ( x d y )  /\  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x
d z ) ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  legval  23015
  Copyright terms: Public domain W3C validator