Definition df-segle 32214

Description: Define the segment length comparison relationship. This relationship expresses that the segment A B is no longer than C D. 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	|- Seg<_ = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) ) }

Distinct variable group:   q, p, n, a, b, c, d, y

Detailed syntax breakdown of Definition df-segle

Step	Hyp	Ref	Expression
1		csegle 32213	. 2 class Seg<_
2		vp	. . . . . . . . . . 11 setvar p
3	2	cv 1482	. . . . . . . . . 10 class p
4		va	. . . . . . . . . . . 12 setvar a
5	4	cv 1482	. . . . . . . . . . 11 class a
6		vb	. . . . . . . . . . . 12 setvar b
7	6	cv 1482	. . . . . . . . . . 11 class b
8	5, 7	cop 4183	. . . . . . . . . 10 class <. a , b >.
9	3, 8	wceq 1483	. . . . . . . . 9 wff p = <. a , b >.
10		vq	. . . . . . . . . . 11 setvar q
11	10	cv 1482	. . . . . . . . . 10 class q
12		vc	. . . . . . . . . . . 12 setvar c
13	12	cv 1482	. . . . . . . . . . 11 class c
14		vd	. . . . . . . . . . . 12 setvar d
15	14	cv 1482	. . . . . . . . . . 11 class d
16	13, 15	cop 4183	. . . . . . . . . 10 class <. c , d >.
17	11, 16	wceq 1483	. . . . . . . . 9 wff q = <. c , d >.
18		vy	. . . . . . . . . . . . 13 setvar y
19	18	cv 1482	. . . . . . . . . . . 12 class y
20		cbtwn 25769	. . . . . . . . . . . 12 class Btwn
21	19, 16, 20	wbr 4653	. . . . . . . . . . 11 wff y Btwn <. c , d >.
22	13, 19	cop 4183	. . . . . . . . . . . 12 class <. c , y >.
23		ccgr 25770	. . . . . . . . . . . 12 class Cgr
24	8, 22, 23	wbr 4653	. . . . . . . . . . 11 wff <. a , b >.Cgr <. c , y >.
25	21, 24	wa 384	. . . . . . . . . 10 wff ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. )
26		vn	. . . . . . . . . . . 12 setvar n
27	26	cv 1482	. . . . . . . . . . 11 class n
28		cee 25768	. . . . . . . . . . 11 class EE
29	27, 28	cfv 5888	. . . . . . . . . 10 class ( EE ` n )
30	25, 18, 29	wrex 2913	. . . . . . . . 9 wff E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. )
31	9, 17, 30	w3a 1037	. . . . . . . 8 wff ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) )
32	31, 14, 29	wrex 2913	. . . . . . 7 wff E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) )
33	32, 12, 29	wrex 2913	. . . . . 6 wff E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) )
34	33, 6, 29	wrex 2913	. . . . 5 wff E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) )
35	34, 4, 29	wrex 2913	. . . 4 wff E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) )
36		cn 11020	. . . 4 class NN
37	35, 26, 36	wrex 2913	. . 3 wff E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) )
38	37, 2, 10	copab 4712	. 2 class { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) ) }
39	1, 38	wceq 1483	1 wff Seg<_ = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) ( p = <. a , b >. /\ q = <. c , d >. /\ E. y e. ( EE ` n ) ( y Btwn <. c , d >. /\ <. a , b >.Cgr <. c , y >. ) ) }

This definition is referenced by:  brsegle  32215