Definition df-trkgc

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 , so it is not listed in this definition. (Contributed by Thierry Arnoux, 24-Aug-2017)

	Ref	Expression
Assertion	df-trkgc	⊢ TarskiGC = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstrkgc	⊢ TarskiGC
1		vf	⊢ 𝑓
2		cbs	⊢ Base
3	1	cv	⊢ 𝑓
4	3 2	cfv	⊢ ( Base ‘ 𝑓 )
5		vp	⊢ 𝑝
6		cds	⊢ dist
7	3 6	cfv	⊢ ( dist ‘ 𝑓 )
8		vd	⊢ 𝑑
9		vx	⊢ 𝑥
10	5	cv	⊢ 𝑝
11		vy	⊢ 𝑦
12	9	cv	⊢ 𝑥
13	8	cv	⊢ 𝑑
14	11	cv	⊢ 𝑦
15	12 14 13	co	⊢ ( 𝑥 𝑑 𝑦 )
16	14 12 13	co	⊢ ( 𝑦 𝑑 𝑥 )
17	15 16	wceq	⊢ ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 )
18	17 11 10	wral	⊢ ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 )
19	18 9 10	wral	⊢ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 )
20		vz	⊢ 𝑧
21	20	cv	⊢ 𝑧
22	21 21 13	co	⊢ ( 𝑧 𝑑 𝑧 )
23	15 22	wceq	⊢ ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 )
24	12 14	wceq	⊢ 𝑥 = 𝑦
25	23 24	wi	⊢ ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 )
26	25 20 10	wral	⊢ ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 )
27	26 11 10	wral	⊢ ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 )
28	27 9 10	wral	⊢ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 )
29	19 28	wa	⊢ ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) )
30	29 8 7	wsbc	⊢ [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) )
31	30 5 4	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) )
32	31 1	cab	⊢ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) }
33	0 32	wceq	⊢ TarskiGC = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) }