Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-segle Structured version   Unicode version

Definition df-segle 26033
 Description: Define the segment length comparison relationship. This relationship expresses that the segment is no longer than . In this section, we establish various properties of this relationship showing that it is a transitive, reflexive relationship on pairs of points that is substitutive under congruence. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 11-Oct-2013.)
Assertion
Ref Expression
df-segle Cgr
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-segle
StepHypRef Expression
1 csegle 26032 . 2
2 vp . . . . . . . . . . 11
32cv 1651 . . . . . . . . . 10
4 va . . . . . . . . . . . 12
54cv 1651 . . . . . . . . . . 11
6 vb . . . . . . . . . . . 12
76cv 1651 . . . . . . . . . . 11
85, 7cop 3809 . . . . . . . . . 10
93, 8wceq 1652 . . . . . . . . 9
10 vq . . . . . . . . . . 11
1110cv 1651 . . . . . . . . . 10
12 vc . . . . . . . . . . . 12
1312cv 1651 . . . . . . . . . . 11
14 vd . . . . . . . . . . . 12
1514cv 1651 . . . . . . . . . . 11
1613, 15cop 3809 . . . . . . . . . 10
1711, 16wceq 1652 . . . . . . . . 9
18 vy . . . . . . . . . . . . 13
1918cv 1651 . . . . . . . . . . . 12
20 cbtwn 25820 . . . . . . . . . . . 12
2119, 16, 20wbr 4204 . . . . . . . . . . 11
2213, 19cop 3809 . . . . . . . . . . . 12
23 ccgr 25821 . . . . . . . . . . . 12 Cgr
248, 22, 23wbr 4204 . . . . . . . . . . 11 Cgr
2521, 24wa 359 . . . . . . . . . 10 Cgr
26 vn . . . . . . . . . . . 12
2726cv 1651 . . . . . . . . . . 11
28 cee 25819 . . . . . . . . . . 11
2927, 28cfv 5446 . . . . . . . . . 10
3025, 18, 29wrex 2698 . . . . . . . . 9 Cgr
319, 17, 30w3a 936 . . . . . . . 8 Cgr
3231, 14, 29wrex 2698 . . . . . . 7 Cgr
3332, 12, 29wrex 2698 . . . . . 6 Cgr
3433, 6, 29wrex 2698 . . . . 5 Cgr
3534, 4, 29wrex 2698 . . . 4 Cgr
36 cn 9992 . . . 4
3735, 26, 36wrex 2698 . . 3 Cgr
3837, 2, 10copab 4257 . 2 Cgr
391, 38wceq 1652 1 Cgr
 Colors of variables: wff set class This definition is referenced by:  brsegle  26034
 Copyright terms: Public domain W3C validator