Definition df-ofs 29567

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 24073). See brofs 29589 and 5segofs 29590 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)

Assertion

Ref

Expression

df-ofs

|- OuterFiveSeg = { <. 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 ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) ) }

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

Detailed syntax breakdown of Definition df-ofs

Step	Hyp	Ref	Expression
1		cofs 29566	. 2 class OuterFiveSeg
2		vp	. . . . . . . . . . . . . . 15 setvar p
3	2	cv 1378	. . . . . . . . . . . . . 14 class p
4		va	. . . . . . . . . . . . . . . . 17 setvar a
5	4	cv 1378	. . . . . . . . . . . . . . . 16 class a
6		vb	. . . . . . . . . . . . . . . . 17 setvar b
7	6	cv 1378	. . . . . . . . . . . . . . . 16 class b
8	5, 7	cop 4039	. . . . . . . . . . . . . . 15 class <. a , b >.
9		vc	. . . . . . . . . . . . . . . . 17 setvar c
10	9	cv 1378	. . . . . . . . . . . . . . . 16 class c
11		vd	. . . . . . . . . . . . . . . . 17 setvar d
12	11	cv 1378	. . . . . . . . . . . . . . . 16 class d
13	10, 12	cop 4039	. . . . . . . . . . . . . . 15 class <. c , d >.
14	8, 13	cop 4039	. . . . . . . . . . . . . 14 class <. <. a , b >. , <. c , d >. >.
15	3, 14	wceq 1379	. . . . . . . . . . . . 13 wff p = <. <. a , b >. , <. c , d >. >.
16		vq	. . . . . . . . . . . . . . 15 setvar q
17	16	cv 1378	. . . . . . . . . . . . . 14 class q
18		vx	. . . . . . . . . . . . . . . . 17 setvar x
19	18	cv 1378	. . . . . . . . . . . . . . . 16 class x
20		vy	. . . . . . . . . . . . . . . . 17 setvar y
21	20	cv 1378	. . . . . . . . . . . . . . . 16 class y
22	19, 21	cop 4039	. . . . . . . . . . . . . . 15 class <. x , y >.
23		vz	. . . . . . . . . . . . . . . . 17 setvar z
24	23	cv 1378	. . . . . . . . . . . . . . . 16 class z
25		vw	. . . . . . . . . . . . . . . . 17 setvar w
26	25	cv 1378	. . . . . . . . . . . . . . . 16 class w
27	24, 26	cop 4039	. . . . . . . . . . . . . . 15 class <. z , w >.
28	22, 27	cop 4039	. . . . . . . . . . . . . 14 class <. <. x , y >. , <. z , w >. >.
29	17, 28	wceq 1379	. . . . . . . . . . . . 13 wff q = <. <. x , y >. , <. z , w >. >.
30	5, 10	cop 4039	. . . . . . . . . . . . . . . 16 class <. a , c >.
31		cbtwn 24024	. . . . . . . . . . . . . . . 16 class Btwn
32	7, 30, 31	wbr 4453	. . . . . . . . . . . . . . 15 wff b Btwn <. a , c >.
33	19, 24	cop 4039	. . . . . . . . . . . . . . . 16 class <. x , z >.
34	21, 33, 31	wbr 4453	. . . . . . . . . . . . . . 15 wff y Btwn <. x , z >.
35	32, 34	wa 369	. . . . . . . . . . . . . 14 wff ( b Btwn <. a , c >. /\ y Btwn <. x , z >. )
36		ccgr 24025	. . . . . . . . . . . . . . . 16 class Cgr
37	8, 22, 36	wbr 4453	. . . . . . . . . . . . . . 15 wff <. a , b >.Cgr <. x , y >.
38	7, 10	cop 4039	. . . . . . . . . . . . . . . 16 class <. b , c >.
39	21, 24	cop 4039	. . . . . . . . . . . . . . . 16 class <. y , z >.
40	38, 39, 36	wbr 4453	. . . . . . . . . . . . . . 15 wff <. b , c >.Cgr <. y , z >.
41	37, 40	wa 369	. . . . . . . . . . . . . 14 wff ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. )
42	5, 12	cop 4039	. . . . . . . . . . . . . . . 16 class <. a , d >.
43	19, 26	cop 4039	. . . . . . . . . . . . . . . 16 class <. x , w >.
44	42, 43, 36	wbr 4453	. . . . . . . . . . . . . . 15 wff <. a , d >.Cgr <. x , w >.
45	7, 12	cop 4039	. . . . . . . . . . . . . . . 16 class <. b , d >.
46	21, 26	cop 4039	. . . . . . . . . . . . . . . 16 class <. y , w >.
47	45, 46, 36	wbr 4453	. . . . . . . . . . . . . . 15 wff <. b , d >.Cgr <. y , w >.
48	44, 47	wa 369	. . . . . . . . . . . . . 14 wff ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. )
49	35, 41, 48	w3a 973	. . . . . . . . . . . . 13 wff ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) )
50	15, 29, 49	w3a 973	. . . . . . . . . . . 12 wff ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
51		vn	. . . . . . . . . . . . . 14 setvar n
52	51	cv 1378	. . . . . . . . . . . . 13 class n
53		cee 24023	. . . . . . . . . . . . 13 class EE
54	52, 53	cfv 5594	. . . . . . . . . . . 12 class ( EE ` n )
55	50, 25, 54	wrex 2818	. . . . . . . . . . 11 wff E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
56	55, 23, 54	wrex 2818	. . . . . . . . . 10 wff E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
57	56, 20, 54	wrex 2818	. . . . . . . . 9 wff E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
58	57, 18, 54	wrex 2818	. . . . . . . 8 wff E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
59	58, 11, 54	wrex 2818	. . . . . . 7 wff E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
60	59, 9, 54	wrex 2818	. . . . . 6 wff E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
61	60, 6, 54	wrex 2818	. . . . 5 wff E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
62	61, 4, 54	wrex 2818	. . . 4 wff E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
63		cn 10548	. . . 4 class NN
64	62, 51, 63	wrex 2818	. . 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 ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) )
65	64, 2, 16	copab 4510	. 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 ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) ) }
66	1, 65	wceq 1379	1 wff OuterFiveSeg = { <. 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 ) E. x e. ( EE ` n ) E. y e. ( EE ` n ) E. z e. ( EE ` n ) E. w e. ( EE ` n ) ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , b >.Cgr <. x , y >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. b , d >.Cgr <. y , w >. ) ) ) }

This definition is referenced by:  brofs  29589