Definition df-trkgc 23600

Description: Define the class of geometries fulfilling the congruence axioms of reflexivity, identity and transitivity. These are axioms A1 to A3 of [Schwabhauser] p. 10. With our distance based notation for congruence, transitivity of congruence boils down to transitivity of equality and is already given by eqtr 2493, so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017.)

Assertion

Ref	Expression
df-trkgc	|- TarskiGC = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) }

Distinct variable group:   f, d, p, x, y, z

Detailed syntax breakdown of Definition df-trkgc

Step	Hyp	Ref	Expression
1		cstrkgc 23582	. 2 class TarskiGC
2		vx	. . . . . . . . . . 11 setvar x
3	2	cv 1378	. . . . . . . . . 10 class x
4		vy	. . . . . . . . . . 11 setvar y
5	4	cv 1378	. . . . . . . . . 10 class y
6		vd	. . . . . . . . . . 11 setvar d
7	6	cv 1378	. . . . . . . . . 10 class d
8	3, 5, 7	co 6284	. . . . . . . . 9 class ( x d y )
9	5, 3, 7	co 6284	. . . . . . . . 9 class ( y d x )
10	8, 9	wceq 1379	. . . . . . . 8 wff ( x d y ) = ( y d x )
11		vp	. . . . . . . . 9 setvar p
12	11	cv 1378	. . . . . . . 8 class p
13	10, 4, 12	wral 2814	. . . . . . 7 wff A. y e. p ( x d y ) = ( y d x )
14	13, 2, 12	wral 2814	. . . . . 6 wff A. x e. p A. y e. p ( x d y ) = ( y d x )
15		vz	. . . . . . . . . . . . 13 setvar z
16	15	cv 1378	. . . . . . . . . . . 12 class z
17	16, 16, 7	co 6284	. . . . . . . . . . 11 class ( z d z )
18	8, 17	wceq 1379	. . . . . . . . . 10 wff ( x d y ) = ( z d z )
19	2, 4	weq 1705	. . . . . . . . . 10 wff x = y
20	18, 19	wi 4	. . . . . . . . 9 wff ( ( x d y ) = ( z d z ) -> x = y )
21	20, 15, 12	wral 2814	. . . . . . . 8 wff A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
22	21, 4, 12	wral 2814	. . . . . . 7 wff A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
23	22, 2, 12	wral 2814	. . . . . 6 wff A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
24	14, 23	wa 369	. . . . 5 wff ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) )
25		vf	. . . . . . 7 setvar f
26	25	cv 1378	. . . . . 6 class f
27		cds 14564	. . . . . 6 class dist
28	26, 27	cfv 5588	. . . . 5 class ( dist ` f )
29	24, 6, 28	wsbc 3331	. . . 4 wff [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) )
30		cbs 14490	. . . . 5 class Base
31	26, 30	cfv 5588	. . . 4 class ( Base ` f )
32	29, 11, 31	wsbc 3331	. . 3 wff [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) )
33	32, 25	cab 2452	. 2 class { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) }
34	1, 33	wceq 1379	1 wff TarskiGC = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. ( A. x e. p A. y e. p ( x d y ) = ( y d x ) /\ A. x e. p A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y ) ) }

This definition is referenced by:  istrkgc  23607