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

Definition df-leg 24174
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 24173 . 2  class ≤G
2 vg . . 3  setvar  g
3 cvv 3106 . . 3  class  _V
4 vf . . . . . . . . . . . 12  setvar  f
54cv 1397 . . . . . . . . . . 11  class  f
6 vx . . . . . . . . . . . . 13  setvar  x
76cv 1397 . . . . . . . . . . . 12  class  x
8 vy . . . . . . . . . . . . 13  setvar  y
98cv 1397 . . . . . . . . . . . 12  class  y
10 vd . . . . . . . . . . . . 13  setvar  d
1110cv 1397 . . . . . . . . . . . 12  class  d
127, 9, 11co 6270 . . . . . . . . . . 11  class  ( x d y )
135, 12wceq 1398 . . . . . . . . . 10  wff  f  =  ( x d y )
14 vz . . . . . . . . . . . . . 14  setvar  z
1514cv 1397 . . . . . . . . . . . . 13  class  z
16 vi . . . . . . . . . . . . . . 15  setvar  i
1716cv 1397 . . . . . . . . . . . . . 14  class  i
187, 9, 17co 6270 . . . . . . . . . . . . 13  class  ( x i y )
1915, 18wcel 1823 . . . . . . . . . . . 12  wff  z  e.  ( x i y )
20 ve . . . . . . . . . . . . . 14  setvar  e
2120cv 1397 . . . . . . . . . . . . 13  class  e
227, 15, 11co 6270 . . . . . . . . . . . . 13  class  ( x d z )
2321, 22wceq 1398 . . . . . . . . . . . 12  wff  e  =  ( x d z )
2419, 23wa 367 . . . . . . . . . . 11  wff  ( z  e.  ( x i y )  /\  e  =  ( x d z ) )
25 vp . . . . . . . . . . . 12  setvar  p
2625cv 1397 . . . . . . . . . . 11  class  p
2724, 14, 26wrex 2805 . . . . . . . . . 10  wff  E. z  e.  p  ( z  e.  ( x i y )  /\  e  =  ( x d z ) )
2813, 27wa 367 . . . . . . . . 9  wff  ( f  =  ( x d y )  /\  E. z  e.  p  (
z  e.  ( x i y )  /\  e  =  ( x
d z ) ) )
2928, 8, 26wrex 2805 . . . . . . . 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 2805 . . . . . . 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 1397 . . . . . . . 8  class  g
32 citv 24033 . . . . . . . 8  class Itv
3331, 32cfv 5570 . . . . . . 7  class  (Itv `  g )
3430, 16, 33wsbc 3324 . . . . . 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 14796 . . . . . . 7  class  dist
3631, 35cfv 5570 . . . . . 6  class  ( dist `  g )
3734, 10, 36wsbc 3324 . . . . 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 14719 . . . . . 6  class  Base
3931, 38cfv 5570 . . . . 5  class  ( Base `  g )
4037, 25, 39wsbc 3324 . . . 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 4496 . . 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 4497 . 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 1398 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  24175
  Copyright terms: Public domain W3C validator