Definition df-ifs 32147

Description: The inner five segment configuration is an abbreviation for another congruence condition. See brifs 32150 and ifscgr 32151 for how it is used. Definition 4.1 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 26-Sep-2013.)

Assertion

Ref

Expression

df-ifs

|- InnerFiveSeg = { <. 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) ) }

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

Detailed syntax breakdown of Definition df-ifs

Step	Hyp	Ref	Expression
1		cifs 32142	. 2 class InnerFiveSeg
2		vp	. . . . . . . . . . . . . . 15 setvar p
3	2	cv 1482	. . . . . . . . . . . . . 14 class p
4		va	. . . . . . . . . . . . . . . . 17 setvar a
5	4	cv 1482	. . . . . . . . . . . . . . . 16 class a
6		vb	. . . . . . . . . . . . . . . . 17 setvar b
7	6	cv 1482	. . . . . . . . . . . . . . . 16 class b
8	5, 7	cop 4183	. . . . . . . . . . . . . . 15 class <. a , b >.
9		vc	. . . . . . . . . . . . . . . . 17 setvar c
10	9	cv 1482	. . . . . . . . . . . . . . . 16 class c
11		vd	. . . . . . . . . . . . . . . . 17 setvar d
12	11	cv 1482	. . . . . . . . . . . . . . . 16 class d
13	10, 12	cop 4183	. . . . . . . . . . . . . . 15 class <. c , d >.
14	8, 13	cop 4183	. . . . . . . . . . . . . 14 class <. <. a , b >. , <. c , d >. >.
15	3, 14	wceq 1483	. . . . . . . . . . . . 13 wff p = <. <. a , b >. , <. c , d >. >.
16		vq	. . . . . . . . . . . . . . 15 setvar q
17	16	cv 1482	. . . . . . . . . . . . . 14 class q
18		vx	. . . . . . . . . . . . . . . . 17 setvar x
19	18	cv 1482	. . . . . . . . . . . . . . . 16 class x
20		vy	. . . . . . . . . . . . . . . . 17 setvar y
21	20	cv 1482	. . . . . . . . . . . . . . . 16 class y
22	19, 21	cop 4183	. . . . . . . . . . . . . . 15 class <. x , y >.
23		vz	. . . . . . . . . . . . . . . . 17 setvar z
24	23	cv 1482	. . . . . . . . . . . . . . . 16 class z
25		vw	. . . . . . . . . . . . . . . . 17 setvar w
26	25	cv 1482	. . . . . . . . . . . . . . . 16 class w
27	24, 26	cop 4183	. . . . . . . . . . . . . . 15 class <. z , w >.
28	22, 27	cop 4183	. . . . . . . . . . . . . 14 class <. <. x , y >. , <. z , w >. >.
29	17, 28	wceq 1483	. . . . . . . . . . . . 13 wff q = <. <. x , y >. , <. z , w >. >.
30	5, 10	cop 4183	. . . . . . . . . . . . . . . 16 class <. a , c >.
31		cbtwn 25769	. . . . . . . . . . . . . . . 16 class Btwn
32	7, 30, 31	wbr 4653	. . . . . . . . . . . . . . 15 wff b Btwn <. a , c >.
33	19, 24	cop 4183	. . . . . . . . . . . . . . . 16 class <. x , z >.
34	21, 33, 31	wbr 4653	. . . . . . . . . . . . . . 15 wff y Btwn <. x , z >.
35	32, 34	wa 384	. . . . . . . . . . . . . 14 wff ( b Btwn <. a , c >. /\ y Btwn <. x , z >. )
36		ccgr 25770	. . . . . . . . . . . . . . . 16 class Cgr
37	30, 33, 36	wbr 4653	. . . . . . . . . . . . . . 15 wff <. a , c >.Cgr <. x , z >.
38	7, 10	cop 4183	. . . . . . . . . . . . . . . 16 class <. b , c >.
39	21, 24	cop 4183	. . . . . . . . . . . . . . . 16 class <. y , z >.
40	38, 39, 36	wbr 4653	. . . . . . . . . . . . . . 15 wff <. b , c >.Cgr <. y , z >.
41	37, 40	wa 384	. . . . . . . . . . . . . 14 wff ( <. a , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. )
42	5, 12	cop 4183	. . . . . . . . . . . . . . . 16 class <. a , d >.
43	19, 26	cop 4183	. . . . . . . . . . . . . . . 16 class <. x , w >.
44	42, 43, 36	wbr 4653	. . . . . . . . . . . . . . 15 wff <. a , d >.Cgr <. x , w >.
45	13, 27, 36	wbr 4653	. . . . . . . . . . . . . . 15 wff <. c , d >.Cgr <. z , w >.
46	44, 45	wa 384	. . . . . . . . . . . . . 14 wff ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. )
47	35, 41, 46	w3a 1037	. . . . . . . . . . . . 13 wff ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) )
48	15, 29, 47	w3a 1037	. . . . . . . . . . . 12 wff ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. x , y >. , <. z , w >. >. /\ ( ( b Btwn <. a , c >. /\ y Btwn <. x , z >. ) /\ ( <. a , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
49		vn	. . . . . . . . . . . . . 14 setvar n
50	49	cv 1482	. . . . . . . . . . . . 13 class n
51		cee 25768	. . . . . . . . . . . . 13 class EE
52	50, 51	cfv 5888	. . . . . . . . . . . 12 class ( EE ` n )
53	48, 25, 52	wrex 2913	. . . . . . . . . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
54	53, 23, 52	wrex 2913	. . . . . . . . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
55	54, 20, 52	wrex 2913	. . . . . . . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
56	55, 18, 52	wrex 2913	. . . . . . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
57	56, 11, 52	wrex 2913	. . . . . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
58	57, 9, 52	wrex 2913	. . . . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
59	58, 6, 52	wrex 2913	. . . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
60	59, 4, 52	wrex 2913	. . . 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
61		cn 11020	. . . 4 class NN
62	60, 49, 61	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 ) 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) )
63	62, 2, 16	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 ) 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) ) }
64	1, 63	wceq 1483	1 wff InnerFiveSeg = { <. 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 , c >.Cgr <. x , z >. /\ <. b , c >.Cgr <. y , z >. ) /\ ( <. a , d >.Cgr <. x , w >. /\ <. c , d >.Cgr <. z , w >. ) ) ) }

This definition is referenced by:  brifs  32150