MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-trkgcb Structured version   Visualization version   GIF version

Definition df-trkgcb 26541
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.)
Assertion
Ref Expression
df-trkgcb TarskiGCB = {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))}
Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑓,𝑝,𝑖,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkgcb
StepHypRef Expression
1 cstrkgcb 26524 . 2 class TarskiGCB
2 vx . . . . . . . . . . . . . . . . . . . 20 setvar 𝑥
32cv 1542 . . . . . . . . . . . . . . . . . . 19 class 𝑥
4 vy . . . . . . . . . . . . . . . . . . . 20 setvar 𝑦
54cv 1542 . . . . . . . . . . . . . . . . . . 19 class 𝑦
63, 5wne 2940 . . . . . . . . . . . . . . . . . 18 wff 𝑥𝑦
7 vz . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑧
87cv 1542 . . . . . . . . . . . . . . . . . . . 20 class 𝑧
9 vi . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑖
109cv 1542 . . . . . . . . . . . . . . . . . . . 20 class 𝑖
113, 8, 10co 7213 . . . . . . . . . . . . . . . . . . 19 class (𝑥𝑖𝑧)
125, 11wcel 2110 . . . . . . . . . . . . . . . . . 18 wff 𝑦 ∈ (𝑥𝑖𝑧)
13 vb . . . . . . . . . . . . . . . . . . . 20 setvar 𝑏
1413cv 1542 . . . . . . . . . . . . . . . . . . 19 class 𝑏
15 va . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑎
1615cv 1542 . . . . . . . . . . . . . . . . . . . 20 class 𝑎
17 vc . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑐
1817cv 1542 . . . . . . . . . . . . . . . . . . . 20 class 𝑐
1916, 18, 10co 7213 . . . . . . . . . . . . . . . . . . 19 class (𝑎𝑖𝑐)
2014, 19wcel 2110 . . . . . . . . . . . . . . . . . 18 wff 𝑏 ∈ (𝑎𝑖𝑐)
216, 12, 20w3a 1089 . . . . . . . . . . . . . . . . 17 wff (𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐))
22 vd . . . . . . . . . . . . . . . . . . . . . 22 setvar 𝑑
2322cv 1542 . . . . . . . . . . . . . . . . . . . . 21 class 𝑑
243, 5, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑥𝑑𝑦)
2516, 14, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑎𝑑𝑏)
2624, 25wceq 1543 . . . . . . . . . . . . . . . . . . 19 wff (𝑥𝑑𝑦) = (𝑎𝑑𝑏)
275, 8, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑦𝑑𝑧)
2814, 18, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑏𝑑𝑐)
2927, 28wceq 1543 . . . . . . . . . . . . . . . . . . 19 wff (𝑦𝑑𝑧) = (𝑏𝑑𝑐)
3026, 29wa 399 . . . . . . . . . . . . . . . . . 18 wff ((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐))
31 vu . . . . . . . . . . . . . . . . . . . . . 22 setvar 𝑢
3231cv 1542 . . . . . . . . . . . . . . . . . . . . 21 class 𝑢
333, 32, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑥𝑑𝑢)
34 vv . . . . . . . . . . . . . . . . . . . . . 22 setvar 𝑣
3534cv 1542 . . . . . . . . . . . . . . . . . . . . 21 class 𝑣
3616, 35, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑎𝑑𝑣)
3733, 36wceq 1543 . . . . . . . . . . . . . . . . . . 19 wff (𝑥𝑑𝑢) = (𝑎𝑑𝑣)
385, 32, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑦𝑑𝑢)
3914, 35, 23co 7213 . . . . . . . . . . . . . . . . . . . 20 class (𝑏𝑑𝑣)
4038, 39wceq 1543 . . . . . . . . . . . . . . . . . . 19 wff (𝑦𝑑𝑢) = (𝑏𝑑𝑣)
4137, 40wa 399 . . . . . . . . . . . . . . . . . 18 wff ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣))
4230, 41wa 399 . . . . . . . . . . . . . . . . 17 wff (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))
4321, 42wa 399 . . . . . . . . . . . . . . . 16 wff ((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣))))
448, 32, 23co 7213 . . . . . . . . . . . . . . . . 17 class (𝑧𝑑𝑢)
4518, 35, 23co 7213 . . . . . . . . . . . . . . . . 17 class (𝑐𝑑𝑣)
4644, 45wceq 1543 . . . . . . . . . . . . . . . 16 wff (𝑧𝑑𝑢) = (𝑐𝑑𝑣)
4743, 46wi 4 . . . . . . . . . . . . . . 15 wff (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
48 vp . . . . . . . . . . . . . . . 16 setvar 𝑝
4948cv 1542 . . . . . . . . . . . . . . 15 class 𝑝
5047, 34, 49wral 3061 . . . . . . . . . . . . . 14 wff 𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5150, 17, 49wral 3061 . . . . . . . . . . . . 13 wff 𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5251, 13, 49wral 3061 . . . . . . . . . . . 12 wff 𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5352, 15, 49wral 3061 . . . . . . . . . . 11 wff 𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5453, 31, 49wral 3061 . . . . . . . . . 10 wff 𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5554, 7, 49wral 3061 . . . . . . . . 9 wff 𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5655, 4, 49wral 3061 . . . . . . . 8 wff 𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5756, 2, 49wral 3061 . . . . . . 7 wff 𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣))
5827, 25wceq 1543 . . . . . . . . . . . . 13 wff (𝑦𝑑𝑧) = (𝑎𝑑𝑏)
5912, 58wa 399 . . . . . . . . . . . 12 wff (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏))
6059, 7, 49wrex 3062 . . . . . . . . . . 11 wff 𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏))
6160, 13, 49wral 3061 . . . . . . . . . 10 wff 𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏))
6261, 15, 49wral 3061 . . . . . . . . 9 wff 𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏))
6362, 4, 49wral 3061 . . . . . . . 8 wff 𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏))
6463, 2, 49wral 3061 . . . . . . 7 wff 𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏))
6557, 64wa 399 . . . . . 6 wff (∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))
66 vf . . . . . . . 8 setvar 𝑓
6766cv 1542 . . . . . . 7 class 𝑓
68 citv 26527 . . . . . . 7 class Itv
6967, 68cfv 6380 . . . . . 6 class (Itv‘𝑓)
7065, 9, 69wsbc 3694 . . . . 5 wff [(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))
71 cds 16811 . . . . . 6 class dist
7267, 71cfv 6380 . . . . 5 class (dist‘𝑓)
7370, 22, 72wsbc 3694 . . . 4 wff [(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))
74 cbs 16760 . . . . 5 class Base
7567, 74cfv 6380 . . . 4 class (Base‘𝑓)
7673, 48, 75wsbc 3694 . . 3 wff [(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))
7776, 66cab 2714 . 2 class {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))}
781, 77wceq 1543 1 wff TarskiGCB = {𝑓[(Base‘𝑓) / 𝑝][(dist‘𝑓) / 𝑑][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑎𝑝𝑏𝑝𝑐𝑝𝑣𝑝 (((𝑥𝑦𝑦 ∈ (𝑥𝑖𝑧) ∧ 𝑏 ∈ (𝑎𝑖𝑐)) ∧ (((𝑥𝑑𝑦) = (𝑎𝑑𝑏) ∧ (𝑦𝑑𝑧) = (𝑏𝑑𝑐)) ∧ ((𝑥𝑑𝑢) = (𝑎𝑑𝑣) ∧ (𝑦𝑑𝑢) = (𝑏𝑑𝑣)))) → (𝑧𝑑𝑢) = (𝑐𝑑𝑣)) ∧ ∀𝑥𝑝𝑦𝑝𝑎𝑝𝑏𝑝𝑧𝑝 (𝑦 ∈ (𝑥𝑖𝑧) ∧ (𝑦𝑑𝑧) = (𝑎𝑑𝑏)))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkgcb  26547
  Copyright terms: Public domain W3C validator