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

Definition df-trkgb 25393
Description: Define the class of geometries fulfilling the 3 betweenness axioms in Tarski's Axiomatization of Geometry: identity, Axiom A6 of [Schwabhauser] p. 11, axiom of Pasch, Axiom A7 of [Schwabhauser] p. 12, and continuity, Axiom A11 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 24-Aug-2017.)
Assertion
Ref Expression
df-trkgb TarskiGB = {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)))}
Distinct variable group:   𝑎,𝑏,𝑓,𝑝,𝑖,𝑠,𝑡,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkgb
StepHypRef Expression
1 cstrkgb 25376 . 2 class TarskiGB
2 vy . . . . . . . . . . 11 setvar 𝑦
32cv 1522 . . . . . . . . . 10 class 𝑦
4 vx . . . . . . . . . . . 12 setvar 𝑥
54cv 1522 . . . . . . . . . . 11 class 𝑥
6 vi . . . . . . . . . . . 12 setvar 𝑖
76cv 1522 . . . . . . . . . . 11 class 𝑖
85, 5, 7co 6690 . . . . . . . . . 10 class (𝑥𝑖𝑥)
93, 8wcel 2030 . . . . . . . . 9 wff 𝑦 ∈ (𝑥𝑖𝑥)
104, 2weq 1931 . . . . . . . . 9 wff 𝑥 = 𝑦
119, 10wi 4 . . . . . . . 8 wff (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦)
12 vp . . . . . . . . 9 setvar 𝑝
1312cv 1522 . . . . . . . 8 class 𝑝
1411, 2, 13wral 2941 . . . . . . 7 wff 𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦)
1514, 4, 13wral 2941 . . . . . 6 wff 𝑥𝑝𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦)
16 vu . . . . . . . . . . . . . . 15 setvar 𝑢
1716cv 1522 . . . . . . . . . . . . . 14 class 𝑢
18 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
1918cv 1522 . . . . . . . . . . . . . . 15 class 𝑧
205, 19, 7co 6690 . . . . . . . . . . . . . 14 class (𝑥𝑖𝑧)
2117, 20wcel 2030 . . . . . . . . . . . . 13 wff 𝑢 ∈ (𝑥𝑖𝑧)
22 vv . . . . . . . . . . . . . . 15 setvar 𝑣
2322cv 1522 . . . . . . . . . . . . . 14 class 𝑣
243, 19, 7co 6690 . . . . . . . . . . . . . 14 class (𝑦𝑖𝑧)
2523, 24wcel 2030 . . . . . . . . . . . . 13 wff 𝑣 ∈ (𝑦𝑖𝑧)
2621, 25wa 383 . . . . . . . . . . . 12 wff (𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧))
27 va . . . . . . . . . . . . . . . 16 setvar 𝑎
2827cv 1522 . . . . . . . . . . . . . . 15 class 𝑎
2917, 3, 7co 6690 . . . . . . . . . . . . . . 15 class (𝑢𝑖𝑦)
3028, 29wcel 2030 . . . . . . . . . . . . . 14 wff 𝑎 ∈ (𝑢𝑖𝑦)
3123, 5, 7co 6690 . . . . . . . . . . . . . . 15 class (𝑣𝑖𝑥)
3228, 31wcel 2030 . . . . . . . . . . . . . 14 wff 𝑎 ∈ (𝑣𝑖𝑥)
3330, 32wa 383 . . . . . . . . . . . . 13 wff (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))
3433, 27, 13wrex 2942 . . . . . . . . . . . 12 wff 𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))
3526, 34wi 4 . . . . . . . . . . 11 wff ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
3635, 22, 13wral 2941 . . . . . . . . . 10 wff 𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
3736, 16, 13wral 2941 . . . . . . . . 9 wff 𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
3837, 18, 13wral 2941 . . . . . . . 8 wff 𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
3938, 2, 13wral 2941 . . . . . . 7 wff 𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
4039, 4, 13wral 2941 . . . . . 6 wff 𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥)))
4128, 3, 7co 6690 . . . . . . . . . . . . 13 class (𝑎𝑖𝑦)
425, 41wcel 2030 . . . . . . . . . . . 12 wff 𝑥 ∈ (𝑎𝑖𝑦)
43 vt . . . . . . . . . . . . 13 setvar 𝑡
4443cv 1522 . . . . . . . . . . . 12 class 𝑡
4542, 2, 44wral 2941 . . . . . . . . . . 11 wff 𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦)
46 vs . . . . . . . . . . . 12 setvar 𝑠
4746cv 1522 . . . . . . . . . . 11 class 𝑠
4845, 4, 47wral 2941 . . . . . . . . . 10 wff 𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦)
4948, 27, 13wrex 2942 . . . . . . . . 9 wff 𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦)
50 vb . . . . . . . . . . . . . 14 setvar 𝑏
5150cv 1522 . . . . . . . . . . . . 13 class 𝑏
525, 3, 7co 6690 . . . . . . . . . . . . 13 class (𝑥𝑖𝑦)
5351, 52wcel 2030 . . . . . . . . . . . 12 wff 𝑏 ∈ (𝑥𝑖𝑦)
5453, 2, 44wral 2941 . . . . . . . . . . 11 wff 𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)
5554, 4, 47wral 2941 . . . . . . . . . 10 wff 𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)
5655, 50, 13wrex 2942 . . . . . . . . 9 wff 𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)
5749, 56wi 4 . . . . . . . 8 wff (∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦))
5813cpw 4191 . . . . . . . 8 class 𝒫 𝑝
5957, 43, 58wral 2941 . . . . . . 7 wff 𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦))
6059, 46, 58wral 2941 . . . . . 6 wff 𝑠 ∈ 𝒫 𝑝𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦))
6115, 40, 60w3a 1054 . . . . 5 wff (∀𝑥𝑝𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)))
62 vf . . . . . . 7 setvar 𝑓
6362cv 1522 . . . . . 6 class 𝑓
64 citv 25380 . . . . . 6 class Itv
6563, 64cfv 5926 . . . . 5 class (Itv‘𝑓)
6661, 6, 65wsbc 3468 . . . 4 wff [(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)))
67 cbs 15904 . . . . 5 class Base
6863, 67cfv 5926 . . . 4 class (Base‘𝑓)
6966, 12, 68wsbc 3468 . . 3 wff [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)))
7069, 62cab 2637 . 2 class {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)))}
711, 70wceq 1523 1 wff TarskiGB = {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](∀𝑥𝑝𝑦𝑝 (𝑦 ∈ (𝑥𝑖𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) → ∃𝑎𝑝 (𝑎 ∈ (𝑢𝑖𝑦) ∧ 𝑎 ∈ (𝑣𝑖𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑝𝑡 ∈ 𝒫 𝑝(∃𝑎𝑝𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝑖𝑦) → ∃𝑏𝑝𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝑖𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkgb  25399
  Copyright terms: Public domain W3C validator