Definition df-afs 30748

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 25364). See df-ofs 32090. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) (Modified by Thierry Arnoux, 15-Mar-2019.)

Assertion

Ref

Expression

df-afs

|- AFS = ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )

Distinct variable group:   a, b, c, d, x, y, z, w, e, f, g, h, i, p

Detailed syntax breakdown of Definition df-afs

Step	Hyp	Ref	Expression
1		cafs 30747	. 2 class AFS
2		vg	. . 3 setvar g
3		cstrkg 25329	. . 3 class TarskiG
4		ve	. . . . . . . . . . . . . . . . . 18 setvar e
5	4	cv 1482	. . . . . . . . . . . . . . . . 17 class e
6		va	. . . . . . . . . . . . . . . . . . . 20 setvar a
7	6	cv 1482	. . . . . . . . . . . . . . . . . . 19 class a
8		vb	. . . . . . . . . . . . . . . . . . . 20 setvar b
9	8	cv 1482	. . . . . . . . . . . . . . . . . . 19 class b
10	7, 9	cop 4183	. . . . . . . . . . . . . . . . . 18 class <. a , b >.
11		vc	. . . . . . . . . . . . . . . . . . . 20 setvar c
12	11	cv 1482	. . . . . . . . . . . . . . . . . . 19 class c
13		vd	. . . . . . . . . . . . . . . . . . . 20 setvar d
14	13	cv 1482	. . . . . . . . . . . . . . . . . . 19 class d
15	12, 14	cop 4183	. . . . . . . . . . . . . . . . . 18 class <. c , d >.
16	10, 15	cop 4183	. . . . . . . . . . . . . . . . 17 class <. <. a , b >. , <. c , d >. >.
17	5, 16	wceq 1483	. . . . . . . . . . . . . . . 16 wff e = <. <. a , b >. , <. c , d >. >.
18		vf	. . . . . . . . . . . . . . . . . 18 setvar f
19	18	cv 1482	. . . . . . . . . . . . . . . . 17 class f
20		vx	. . . . . . . . . . . . . . . . . . . 20 setvar x
21	20	cv 1482	. . . . . . . . . . . . . . . . . . 19 class x
22		vy	. . . . . . . . . . . . . . . . . . . 20 setvar y
23	22	cv 1482	. . . . . . . . . . . . . . . . . . 19 class y
24	21, 23	cop 4183	. . . . . . . . . . . . . . . . . 18 class <. x , y >.
25		vz	. . . . . . . . . . . . . . . . . . . 20 setvar z
26	25	cv 1482	. . . . . . . . . . . . . . . . . . 19 class z
27		vw	. . . . . . . . . . . . . . . . . . . 20 setvar w
28	27	cv 1482	. . . . . . . . . . . . . . . . . . 19 class w
29	26, 28	cop 4183	. . . . . . . . . . . . . . . . . 18 class <. z , w >.
30	24, 29	cop 4183	. . . . . . . . . . . . . . . . 17 class <. <. x , y >. , <. z , w >. >.
31	19, 30	wceq 1483	. . . . . . . . . . . . . . . 16 wff f = <. <. x , y >. , <. z , w >. >.
32		vi	. . . . . . . . . . . . . . . . . . . . 21 setvar i
33	32	cv 1482	. . . . . . . . . . . . . . . . . . . 20 class i
34	7, 12, 33	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( a i c )
35	9, 34	wcel 1990	. . . . . . . . . . . . . . . . . 18 wff b e. ( a i c )
36	21, 26, 33	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( x i z )
37	23, 36	wcel 1990	. . . . . . . . . . . . . . . . . 18 wff y e. ( x i z )
38	35, 37	wa 384	. . . . . . . . . . . . . . . . 17 wff ( b e. ( a i c ) /\ y e. ( x i z ) )
39		vh	. . . . . . . . . . . . . . . . . . . . 21 setvar h
40	39	cv 1482	. . . . . . . . . . . . . . . . . . . 20 class h
41	7, 9, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( a h b )
42	21, 23, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( x h y )
43	41, 42	wceq 1483	. . . . . . . . . . . . . . . . . 18 wff ( a h b ) = ( x h y )
44	9, 12, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( b h c )
45	23, 26, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( y h z )
46	44, 45	wceq 1483	. . . . . . . . . . . . . . . . . 18 wff ( b h c ) = ( y h z )
47	43, 46	wa 384	. . . . . . . . . . . . . . . . 17 wff ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) )
48	7, 14, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( a h d )
49	21, 28, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( x h w )
50	48, 49	wceq 1483	. . . . . . . . . . . . . . . . . 18 wff ( a h d ) = ( x h w )
51	9, 14, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( b h d )
52	23, 28, 40	co 6650	. . . . . . . . . . . . . . . . . . 19 class ( y h w )
53	51, 52	wceq 1483	. . . . . . . . . . . . . . . . . 18 wff ( b h d ) = ( y h w )
54	50, 53	wa 384	. . . . . . . . . . . . . . . . 17 wff ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) )
55	38, 47, 54	w3a 1037	. . . . . . . . . . . . . . . 16 wff ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) )
56	17, 31, 55	w3a 1037	. . . . . . . . . . . . . . 15 wff ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
57		vp	. . . . . . . . . . . . . . . 16 setvar p
58	57	cv 1482	. . . . . . . . . . . . . . 15 class p
59	56, 27, 58	wrex 2913	. . . . . . . . . . . . . 14 wff E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
60	59, 25, 58	wrex 2913	. . . . . . . . . . . . 13 wff E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
61	60, 22, 58	wrex 2913	. . . . . . . . . . . 12 wff E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
62	61, 20, 58	wrex 2913	. . . . . . . . . . 11 wff E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
63	62, 13, 58	wrex 2913	. . . . . . . . . 10 wff E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
64	63, 11, 58	wrex 2913	. . . . . . . . 9 wff E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
65	64, 8, 58	wrex 2913	. . . . . . . 8 wff E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
66	65, 6, 58	wrex 2913	. . . . . . 7 wff E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
67	2	cv 1482	. . . . . . . 8 class g
68		citv 25335	. . . . . . . 8 class Itv
69	67, 68	cfv 5888	. . . . . . 7 class (Itv ` g )
70	66, 32, 69	wsbc 3435	. . . . . 6 wff [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
71		cds 15950	. . . . . . 7 class dist
72	67, 71	cfv 5888	. . . . . 6 class ( dist ` g )
73	70, 39, 72	wsbc 3435	. . . . 5 wff [. ( dist ` g ) / h ]. [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
74		cbs 15857	. . . . . 6 class Base
75	67, 74	cfv 5888	. . . . 5 class ( Base ` g )
76	73, 57, 75	wsbc 3435	. . . 4 wff [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
77	76, 4, 18	copab 4712	. . 3 class { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) }
78	2, 3, 77	cmpt 4729	. 2 class ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )
79	1, 78	wceq 1483	1 wff AFS = ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. (Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )

This definition is referenced by:  afsval  30749