Definition df-trkgb 24043

Description: Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.)

Assertion

Ref	Expression
df-trkgb	|- TarskiGB = { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) }

Distinct variable group:   a, b, f, p, i, s, t, u, v, x, y, z

Detailed syntax breakdown of Definition df-trkgb

Step	Hyp	Ref	Expression
1		cstrkgb 24025	. 2 class TarskiGB
2		vy	. . . . . . . . . . 11 setvar y
3	2	cv 1397	. . . . . . . . . 10 class y
4		vx	. . . . . . . . . . . 12 setvar x
5	4	cv 1397	. . . . . . . . . . 11 class x
6		vi	. . . . . . . . . . . 12 setvar i
7	6	cv 1397	. . . . . . . . . . 11 class i
8	5, 5, 7	co 6270	. . . . . . . . . 10 class ( x i x )
9	3, 8	wcel 1823	. . . . . . . . 9 wff y e. ( x i x )
10	4, 2	weq 1738	. . . . . . . . 9 wff x = y
11	9, 10	wi 4	. . . . . . . 8 wff ( y e. ( x i x ) -> x = y )
12		vp	. . . . . . . . 9 setvar p
13	12	cv 1397	. . . . . . . 8 class p
14	11, 2, 13	wral 2804	. . . . . . 7 wff A. y e. p ( y e. ( x i x ) -> x = y )
15	14, 4, 13	wral 2804	. . . . . 6 wff A. x e. p A. y e. p ( y e. ( x i x ) -> x = y )
16		vu	. . . . . . . . . . . . . . 15 setvar u
17	16	cv 1397	. . . . . . . . . . . . . 14 class u
18		vz	. . . . . . . . . . . . . . . 16 setvar z
19	18	cv 1397	. . . . . . . . . . . . . . 15 class z
20	5, 19, 7	co 6270	. . . . . . . . . . . . . 14 class ( x i z )
21	17, 20	wcel 1823	. . . . . . . . . . . . 13 wff u e. ( x i z )
22		vv	. . . . . . . . . . . . . . 15 setvar v
23	22	cv 1397	. . . . . . . . . . . . . 14 class v
24	3, 19, 7	co 6270	. . . . . . . . . . . . . 14 class ( y i z )
25	23, 24	wcel 1823	. . . . . . . . . . . . 13 wff v e. ( y i z )
26	21, 25	wa 367	. . . . . . . . . . . 12 wff ( u e. ( x i z ) /\ v e. ( y i z ) )
27		va	. . . . . . . . . . . . . . . 16 setvar a
28	27	cv 1397	. . . . . . . . . . . . . . 15 class a
29	17, 3, 7	co 6270	. . . . . . . . . . . . . . 15 class ( u i y )
30	28, 29	wcel 1823	. . . . . . . . . . . . . 14 wff a e. ( u i y )
31	23, 5, 7	co 6270	. . . . . . . . . . . . . . 15 class ( v i x )
32	28, 31	wcel 1823	. . . . . . . . . . . . . 14 wff a e. ( v i x )
33	30, 32	wa 367	. . . . . . . . . . . . 13 wff ( a e. ( u i y ) /\ a e. ( v i x ) )
34	33, 27, 13	wrex 2805	. . . . . . . . . . . 12 wff E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) )
35	26, 34	wi 4	. . . . . . . . . . 11 wff ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) )
36	35, 22, 13	wral 2804	. . . . . . . . . 10 wff A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) )
37	36, 16, 13	wral 2804	. . . . . . . . 9 wff A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) )
38	37, 18, 13	wral 2804	. . . . . . . 8 wff A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) )
39	38, 2, 13	wral 2804	. . . . . . 7 wff A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) )
40	39, 4, 13	wral 2804	. . . . . 6 wff A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) )
41	28, 3, 7	co 6270	. . . . . . . . . . . . 13 class ( a i y )
42	5, 41	wcel 1823	. . . . . . . . . . . 12 wff x e. ( a i y )
43		vt	. . . . . . . . . . . . 13 setvar t
44	43	cv 1397	. . . . . . . . . . . 12 class t
45	42, 2, 44	wral 2804	. . . . . . . . . . 11 wff A. y e. t x e. ( a i y )
46		vs	. . . . . . . . . . . 12 setvar s
47	46	cv 1397	. . . . . . . . . . 11 class s
48	45, 4, 47	wral 2804	. . . . . . . . . 10 wff A. x e. s A. y e. t x e. ( a i y )
49	48, 27, 13	wrex 2805	. . . . . . . . 9 wff E. a e. p A. x e. s A. y e. t x e. ( a i y )
50		vb	. . . . . . . . . . . . . 14 setvar b
51	50	cv 1397	. . . . . . . . . . . . 13 class b
52	5, 3, 7	co 6270	. . . . . . . . . . . . 13 class ( x i y )
53	51, 52	wcel 1823	. . . . . . . . . . . 12 wff b e. ( x i y )
54	53, 2, 44	wral 2804	. . . . . . . . . . 11 wff A. y e. t b e. ( x i y )
55	54, 4, 47	wral 2804	. . . . . . . . . 10 wff A. x e. s A. y e. t b e. ( x i y )
56	55, 50, 13	wrex 2805	. . . . . . . . 9 wff E. b e. p A. x e. s A. y e. t b e. ( x i y )
57	49, 56	wi 4	. . . . . . . 8 wff ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) )
58	13	cpw 3999	. . . . . . . 8 class ~P p
59	57, 43, 58	wral 2804	. . . . . . 7 wff A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) )
60	59, 46, 58	wral 2804	. . . . . 6 wff A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) )
61	15, 40, 60	w3a 971	. . . . 5 wff ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) )
62		vf	. . . . . . 7 setvar f
63	62	cv 1397	. . . . . 6 class f
64		citv 24030	. . . . . 6 class Itv
65	63, 64	cfv 5570	. . . . 5 class (Itv ` f )
66	61, 6, 65	wsbc 3324	. . . 4 wff [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) )
67		cbs 14716	. . . . 5 class Base
68	63, 67	cfv 5570	. . . 4 class ( Base ` f )
69	66, 12, 68	wsbc 3324	. . 3 wff [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) )
70	69, 62	cab 2439	. 2 class { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) }
71	1, 70	wceq 1398	1 wff TarskiGB = { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) }

This definition is referenced by:  istrkgb  24050