Definition df-trkgcb 25349

Description: Define the class of geometries fulfilling the five segment axiom, Axiom A5 of [Schwabhauser] p. 11, and segment construction axiom, Axiom A4 of [Schwabhauser] p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019.)

Assertion

Ref

Expression

df-trkgcb

|- TarskiGCB = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p A. z e. p A. u e. p A. a e. p A. b e. p A. c e. p A. v e. p ( ( ( x =/= y /\ y e. ( x i z ) /\ b e. ( a i c ) ) /\ ( ( ( x d y ) = ( a d b ) /\ ( y d z ) = ( b d c ) ) /\ ( ( x d u ) = ( a d v ) /\ ( y d u ) = ( b d v ) ) ) ) -> ( z d u ) = ( c d v ) ) /\ A. x e. p A. y e. p A. a e. p A. b e. p E. z e. p ( y e. ( x i z ) /\ ( y d z ) = ( a d b ) ) ) }

Distinct variable group:   a, b, c, d, f, p, i, u, v, x, y, z

Detailed syntax breakdown of Definition df-trkgcb

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

This definition is referenced by:  istrkgcb  25355