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

Definition df-segle 24730
 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 24729 . 2
2 vp . . . . . . . . . . 11
32cv 1622 . . . . . . . . . 10
4 va . . . . . . . . . . . 12
54cv 1622 . . . . . . . . . . 11
6 vb . . . . . . . . . . . 12
76cv 1622 . . . . . . . . . . 11
85, 7cop 3643 . . . . . . . . . 10
93, 8wceq 1623 . . . . . . . . 9
10 vq . . . . . . . . . . 11
1110cv 1622 . . . . . . . . . 10
12 vc . . . . . . . . . . . 12
1312cv 1622 . . . . . . . . . . 11
14 vd . . . . . . . . . . . 12
1514cv 1622 . . . . . . . . . . 11
1613, 15cop 3643 . . . . . . . . . 10
1711, 16wceq 1623 . . . . . . . . 9
18 vy . . . . . . . . . . . . 13
1918cv 1622 . . . . . . . . . . . 12
20 cbtwn 24517 . . . . . . . . . . . 12
2119, 16, 20wbr 4023 . . . . . . . . . . 11
2213, 19cop 3643 . . . . . . . . . . . 12
23 ccgr 24518 . . . . . . . . . . . 12 Cgr
248, 22, 23wbr 4023 . . . . . . . . . . 11 Cgr
2521, 24wa 358 . . . . . . . . . 10 Cgr
26 vn . . . . . . . . . . . 12
2726cv 1622 . . . . . . . . . . 11
28 cee 24516 . . . . . . . . . . 11
2927, 28cfv 5255 . . . . . . . . . 10
3025, 18, 29wrex 2544 . . . . . . . . 9 Cgr
319, 17, 30w3a 934 . . . . . . . 8 Cgr
3231, 14, 29wrex 2544 . . . . . . 7 Cgr
3332, 12, 29wrex 2544 . . . . . 6 Cgr
3433, 6, 29wrex 2544 . . . . 5 Cgr
3534, 4, 29wrex 2544 . . . 4 Cgr
36 cn 9746 . . . 4
3735, 26, 36wrex 2544 . . 3 Cgr
3837, 2, 10copab 4076 . 2 Cgr
391, 38wceq 1623 1 Cgr
 Colors of variables: wff set class This definition is referenced by:  brsegle  24731
 Copyright terms: Public domain W3C validator