Metamath Proof Explorer

Definition df-trkgcb

Description: Define the class of geometries fulfilling the five segment axiom, Axiom A5 of Schwabhauser p. 11, and segment construction axiom, Axiom A4 of Schwabhauser p. 11. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Assertion df-trkgcb ⊢𝒢TarskiCB=f|[˙Basef/p]˙[˙dist⁡f/d]˙[˙Itv⁡f/i]˙∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv∧∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkgcb class𝒢TarskiCB
1 vf setvarf
2 cbs classBase
3 1 cv setvarf
4 3 2 cfv classBasef
5 vp setvarp
6 cds classdist
7 3 6 cfv classdist⁡f
8 vd setvard
9 citv classItv
10 3 9 cfv classItv⁡f
11 vi setvari
12 vx setvarx
13 5 cv setvarp
14 vy setvary
15 vz setvarz
16 vu setvaru
17 va setvara
18 vb setvarb
19 vc setvarc
20 vv setvarv
21 12 cv setvarx
22 14 cv setvary
23 21 22 wne wffx≠y
24 11 cv setvari
25 15 cv setvarz
26 21 25 24 co classxiz
27 22 26 wcel wffy∈xiz
28 18 cv setvarb
29 17 cv setvara
30 19 cv setvarc
31 29 30 24 co classaic
32 28 31 wcel wffb∈aic
33 23 27 32 w3a wffx≠y∧y∈xiz∧b∈aic
34 8 cv setvard
35 21 22 34 co classxdy
36 29 28 34 co classadb
37 35 36 wceq wffxdy=adb
38 22 25 34 co classydz
39 28 30 34 co classbdc
40 38 39 wceq wffydz=bdc
41 37 40 wa wffxdy=adb∧ydz=bdc
42 16 cv setvaru
43 21 42 34 co classxdu
44 20 cv setvarv
45 29 44 34 co classadv
46 43 45 wceq wffxdu=adv
47 22 42 34 co classydu
48 28 44 34 co classbdv
49 47 48 wceq wffydu=bdv
50 46 49 wa wffxdu=adv∧ydu=bdv
51 41 50 wa wffxdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv
52 33 51 wa wffx≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv
53 25 42 34 co classzdu
54 30 44 34 co classcdv
55 53 54 wceq wffzdu=cdv
56 52 55 wi wffx≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
57 56 20 13 wral wff∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
58 57 19 13 wral wff∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
59 58 18 13 wral wff∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
60 59 17 13 wral wff∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
61 60 16 13 wral wff∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
62 61 15 13 wral wff∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
63 62 14 13 wral wff∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
64 63 12 13 wral wff∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv
65 38 36 wceq wffydz=adb
66 27 65 wa wffy∈xiz∧ydz=adb
67 66 15 13 wrex wff∃z∈py∈xiz∧ydz=adb
68 67 18 13 wral wff∀b∈p∃z∈py∈xiz∧ydz=adb
69 68 17 13 wral wff∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
70 69 14 13 wral wff∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
71 70 12 13 wral wff∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
72 64 71 wa wff∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv∧∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
73 72 11 10 wsbc wff[˙Itv⁡f/i]˙∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv∧∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
74 73 8 7 wsbc wff[˙dist⁡f/d]˙[˙Itv⁡f/i]˙∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv∧∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
75 74 5 4 wsbc wff[˙Basef/p]˙[˙dist⁡f/d]˙[˙Itv⁡f/i]˙∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv∧∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
76 75 1 cab classf|[˙Basef/p]˙[˙dist⁡f/d]˙[˙Itv⁡f/i]˙∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv∧∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb
77 0 76 wceq wff𝒢TarskiCB=f|[˙Basef/p]˙[˙dist⁡f/d]˙[˙Itv⁡f/i]˙∀x∈p∀y∈p∀z∈p∀u∈p∀a∈p∀b∈p∀c∈p∀v∈px≠y∧y∈xiz∧b∈aic∧xdy=adb∧ydz=bdc∧xdu=adv∧ydu=bdv→zdu=cdv∧∀x∈p∀y∈p∀a∈p∀b∈p∃z∈py∈xiz∧ydz=adb