Definition df-trkgc 26236

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

Assertion

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

Distinct variable group:   𝑓,𝑑,𝑝,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkgc

Step	Hyp	Ref	Expression
1		cstrkgc 26219	. 2 class TarskiGC
2		vx	. . . . . . . . . . 11 setvar 𝑥
3	2	cv 1536	. . . . . . . . . 10 class 𝑥
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1536	. . . . . . . . . 10 class 𝑦
6		vd	. . . . . . . . . . 11 setvar 𝑑
7	6	cv 1536	. . . . . . . . . 10 class 𝑑
8	3, 5, 7	co 7158	. . . . . . . . 9 class (𝑥𝑑𝑦)
9	5, 3, 7	co 7158	. . . . . . . . 9 class (𝑦𝑑𝑥)
10	8, 9	wceq 1537	. . . . . . . 8 wff (𝑥𝑑𝑦) = (𝑦𝑑𝑥)
11		vp	. . . . . . . . 9 setvar 𝑝
12	11	cv 1536	. . . . . . . 8 class 𝑝
13	10, 4, 12	wral 3140	. . . . . . 7 wff ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥)
14	13, 2, 12	wral 3140	. . . . . 6 wff ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥)
15		vz	. . . . . . . . . . . . 13 setvar 𝑧
16	15	cv 1536	. . . . . . . . . . . 12 class 𝑧
17	16, 16, 7	co 7158	. . . . . . . . . . 11 class (𝑧𝑑𝑧)
18	8, 17	wceq 1537	. . . . . . . . . 10 wff (𝑥𝑑𝑦) = (𝑧𝑑𝑧)
19	2, 4	weq 1964	. . . . . . . . . 10 wff 𝑥 = 𝑦
20	18, 19	wi 4	. . . . . . . . 9 wff ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
21	20, 15, 12	wral 3140	. . . . . . . 8 wff ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
22	21, 4, 12	wral 3140	. . . . . . 7 wff ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
23	22, 2, 12	wral 3140	. . . . . 6 wff ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦)
24	14, 23	wa 398	. . . . 5 wff (∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))
25		vf	. . . . . . 7 setvar 𝑓
26	25	cv 1536	. . . . . 6 class 𝑓
27		cds 16576	. . . . . 6 class dist
28	26, 27	cfv 6357	. . . . 5 class (dist‘𝑓)
29	24, 6, 28	wsbc 3774	. . . 4 wff [(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))
30		cbs 16485	. . . . 5 class Base
31	26, 30	cfv 6357	. . . 4 class (Base‘𝑓)
32	29, 11, 31	wsbc 3774	. . 3 wff [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))
33	32, 25	cab 2801	. 2 class {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))}
34	1, 33	wceq 1537	1 wff TarskiGC = {𝑓 ∣ [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑](∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 (𝑥𝑑𝑦) = (𝑦𝑑𝑥) ∧ ∀𝑥 ∈ 𝑝 ∀𝑦 ∈ 𝑝 ∀𝑧 ∈ 𝑝 ((𝑥𝑑𝑦) = (𝑧𝑑𝑧) → 𝑥 = 𝑦))}

This definition is referenced by:  istrkgc  26242