Definition df-trkgc 22921

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 2460, 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 22902	. 2 class TarskiGC
2		vx	. . . . . . . . . . 11 setvar x
3	2	cv 1368	. . . . . . . . . 10 class x
4		vy	. . . . . . . . . . 11 setvar y
5	4	cv 1368	. . . . . . . . . 10 class y
6		vd	. . . . . . . . . . 11 setvar d
7	6	cv 1368	. . . . . . . . . 10 class d
8	3, 5, 7	co 6103	. . . . . . . . 9 class ( x d y )
9	5, 3, 7	co 6103	. . . . . . . . 9 class ( y d x )
10	8, 9	wceq 1369	. . . . . . . 8 wff ( x d y ) = ( y d x )
11		vp	. . . . . . . . 9 setvar p
12	11	cv 1368	. . . . . . . 8 class p
13	10, 4, 12	wral 2727	. . . . . . 7 wff A. y e. p ( x d y ) = ( y d x )
14	13, 2, 12	wral 2727	. . . . . 6 wff A. x e. p A. y e. p ( x d y ) = ( y d x )
15		vz	. . . . . . . . . . . . 13 setvar z
16	15	cv 1368	. . . . . . . . . . . 12 class z
17	16, 16, 7	co 6103	. . . . . . . . . . 11 class ( z d z )
18	8, 17	wceq 1369	. . . . . . . . . 10 wff ( x d y ) = ( z d z )
19	2, 4	weq 1695	. . . . . . . . . 10 wff x = y
20	18, 19	wi 4	. . . . . . . . 9 wff ( ( x d y ) = ( z d z ) -> x = y )
21	20, 15, 12	wral 2727	. . . . . . . 8 wff A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
22	21, 4, 12	wral 2727	. . . . . . 7 wff A. y e. p A. z e. p ( ( x d y ) = ( z d z ) -> x = y )
23	22, 2, 12	wral 2727	. . . . . 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 1368	. . . . . 6 class f
27		cds 14259	. . . . . 6 class dist
28	26, 27	cfv 5430	. . . . 5 class ( dist ` f )
29	24, 6, 28	wsbc 3198	. . . 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 14186	. . . . 5 class Base
31	26, 30	cfv 5430	. . . 4 class ( Base ` f )
32	29, 11, 31	wsbc 3198	. . 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 2429	. 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 1369	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  22929