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 27967
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 27947 . 2 class TarskiGB
2 vy . . . . . . . . . . 11 setvar 𝑦
32cv 1538 . . . . . . . . . 10 class 𝑦
4 vx . . . . . . . . . . . 12 setvar π‘₯
54cv 1538 . . . . . . . . . . 11 class π‘₯
6 vi . . . . . . . . . . . 12 setvar 𝑖
76cv 1538 . . . . . . . . . . 11 class 𝑖
85, 5, 7co 7411 . . . . . . . . . 10 class (π‘₯𝑖π‘₯)
93, 8wcel 2104 . . . . . . . . 9 wff 𝑦 ∈ (π‘₯𝑖π‘₯)
104, 2weq 1964 . . . . . . . . 9 wff π‘₯ = 𝑦
119, 10wi 4 . . . . . . . 8 wff (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦)
12 vp . . . . . . . . 9 setvar 𝑝
1312cv 1538 . . . . . . . 8 class 𝑝
1411, 2, 13wral 3059 . . . . . . 7 wff βˆ€π‘¦ ∈ 𝑝 (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦)
1514, 4, 13wral 3059 . . . . . 6 wff βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦)
16 vu . . . . . . . . . . . . . . 15 setvar 𝑒
1716cv 1538 . . . . . . . . . . . . . 14 class 𝑒
18 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
1918cv 1538 . . . . . . . . . . . . . . 15 class 𝑧
205, 19, 7co 7411 . . . . . . . . . . . . . 14 class (π‘₯𝑖𝑧)
2117, 20wcel 2104 . . . . . . . . . . . . 13 wff 𝑒 ∈ (π‘₯𝑖𝑧)
22 vv . . . . . . . . . . . . . . 15 setvar 𝑣
2322cv 1538 . . . . . . . . . . . . . 14 class 𝑣
243, 19, 7co 7411 . . . . . . . . . . . . . 14 class (𝑦𝑖𝑧)
2523, 24wcel 2104 . . . . . . . . . . . . 13 wff 𝑣 ∈ (𝑦𝑖𝑧)
2621, 25wa 394 . . . . . . . . . . . 12 wff (𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧))
27 va . . . . . . . . . . . . . . . 16 setvar π‘Ž
2827cv 1538 . . . . . . . . . . . . . . 15 class π‘Ž
2917, 3, 7co 7411 . . . . . . . . . . . . . . 15 class (𝑒𝑖𝑦)
3028, 29wcel 2104 . . . . . . . . . . . . . 14 wff π‘Ž ∈ (𝑒𝑖𝑦)
3123, 5, 7co 7411 . . . . . . . . . . . . . . 15 class (𝑣𝑖π‘₯)
3228, 31wcel 2104 . . . . . . . . . . . . . 14 wff π‘Ž ∈ (𝑣𝑖π‘₯)
3330, 32wa 394 . . . . . . . . . . . . 13 wff (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯))
3433, 27, 13wrex 3068 . . . . . . . . . . . 12 wff βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯))
3526, 34wi 4 . . . . . . . . . . 11 wff ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯)))
3635, 22, 13wral 3059 . . . . . . . . . 10 wff βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯)))
3736, 16, 13wral 3059 . . . . . . . . 9 wff βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯)))
3837, 18, 13wral 3059 . . . . . . . 8 wff βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯)))
3938, 2, 13wral 3059 . . . . . . 7 wff βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯)))
4039, 4, 13wral 3059 . . . . . 6 wff βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯)))
4128, 3, 7co 7411 . . . . . . . . . . . . 13 class (π‘Žπ‘–π‘¦)
425, 41wcel 2104 . . . . . . . . . . . 12 wff π‘₯ ∈ (π‘Žπ‘–π‘¦)
43 vt . . . . . . . . . . . . 13 setvar 𝑑
4443cv 1538 . . . . . . . . . . . 12 class 𝑑
4542, 2, 44wral 3059 . . . . . . . . . . 11 wff βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦)
46 vs . . . . . . . . . . . 12 setvar 𝑠
4746cv 1538 . . . . . . . . . . 11 class 𝑠
4845, 4, 47wral 3059 . . . . . . . . . 10 wff βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦)
4948, 27, 13wrex 3068 . . . . . . . . 9 wff βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦)
50 vb . . . . . . . . . . . . . 14 setvar 𝑏
5150cv 1538 . . . . . . . . . . . . 13 class 𝑏
525, 3, 7co 7411 . . . . . . . . . . . . 13 class (π‘₯𝑖𝑦)
5351, 52wcel 2104 . . . . . . . . . . . 12 wff 𝑏 ∈ (π‘₯𝑖𝑦)
5453, 2, 44wral 3059 . . . . . . . . . . 11 wff βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)
5554, 4, 47wral 3059 . . . . . . . . . 10 wff βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)
5655, 50, 13wrex 3068 . . . . . . . . 9 wff βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)
5749, 56wi 4 . . . . . . . 8 wff (βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦))
5813cpw 4601 . . . . . . . 8 class 𝒫 𝑝
5957, 43, 58wral 3059 . . . . . . 7 wff βˆ€π‘‘ ∈ 𝒫 𝑝(βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦))
6059, 46, 58wral 3059 . . . . . 6 wff βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑝(βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦))
6115, 40, 60w3a 1085 . . . . 5 wff (βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑝(βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)))
62 vf . . . . . . 7 setvar 𝑓
6362cv 1538 . . . . . 6 class 𝑓
64 citv 27951 . . . . . 6 class Itv
6563, 64cfv 6542 . . . . 5 class (Itvβ€˜π‘“)
6661, 6, 65wsbc 3776 . . . 4 wff [(Itvβ€˜π‘“) / 𝑖](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑝(βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)))
67 cbs 17148 . . . . 5 class Base
6863, 67cfv 6542 . . . 4 class (Baseβ€˜π‘“)
6966, 12, 68wsbc 3776 . . 3 wff [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑝(βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)))
7069, 62cab 2707 . 2 class {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑝(βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)))}
711, 70wceq 1539 1 wff TarskiGB = {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 (𝑦 ∈ (π‘₯𝑖π‘₯) β†’ π‘₯ = 𝑦) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((𝑒 ∈ (π‘₯𝑖𝑧) ∧ 𝑣 ∈ (𝑦𝑖𝑧)) β†’ βˆƒπ‘Ž ∈ 𝑝 (π‘Ž ∈ (𝑒𝑖𝑦) ∧ π‘Ž ∈ (𝑣𝑖π‘₯))) ∧ βˆ€π‘  ∈ 𝒫 π‘βˆ€π‘‘ ∈ 𝒫 𝑝(βˆƒπ‘Ž ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 π‘₯ ∈ (π‘Žπ‘–π‘¦) β†’ βˆƒπ‘ ∈ 𝑝 βˆ€π‘₯ ∈ 𝑠 βˆ€π‘¦ ∈ 𝑑 𝑏 ∈ (π‘₯𝑖𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkgb  27973
  Copyright terms: Public domain W3C validator