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

Definition df-trkge 25549
Description: Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.)
Assertion
Ref Expression
df-trkge TarskiGE = {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))}
Distinct variable group:   𝑎,𝑏,𝑓,𝑝,𝑖,𝑢,𝑣,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkge
StepHypRef Expression
1 cstrkge 25533 . 2 class TarskiGE
2 vu . . . . . . . . . . . . . 14 setvar 𝑢
32cv 1631 . . . . . . . . . . . . 13 class 𝑢
4 vx . . . . . . . . . . . . . . 15 setvar 𝑥
54cv 1631 . . . . . . . . . . . . . 14 class 𝑥
6 vv . . . . . . . . . . . . . . 15 setvar 𝑣
76cv 1631 . . . . . . . . . . . . . 14 class 𝑣
8 vi . . . . . . . . . . . . . . 15 setvar 𝑖
98cv 1631 . . . . . . . . . . . . . 14 class 𝑖
105, 7, 9co 6813 . . . . . . . . . . . . 13 class (𝑥𝑖𝑣)
113, 10wcel 2139 . . . . . . . . . . . 12 wff 𝑢 ∈ (𝑥𝑖𝑣)
12 vy . . . . . . . . . . . . . . 15 setvar 𝑦
1312cv 1631 . . . . . . . . . . . . . 14 class 𝑦
14 vz . . . . . . . . . . . . . . 15 setvar 𝑧
1514cv 1631 . . . . . . . . . . . . . 14 class 𝑧
1613, 15, 9co 6813 . . . . . . . . . . . . 13 class (𝑦𝑖𝑧)
173, 16wcel 2139 . . . . . . . . . . . 12 wff 𝑢 ∈ (𝑦𝑖𝑧)
185, 3wne 2932 . . . . . . . . . . . 12 wff 𝑥𝑢
1911, 17, 18w3a 1072 . . . . . . . . . . 11 wff (𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢)
20 va . . . . . . . . . . . . . . . . 17 setvar 𝑎
2120cv 1631 . . . . . . . . . . . . . . . 16 class 𝑎
225, 21, 9co 6813 . . . . . . . . . . . . . . 15 class (𝑥𝑖𝑎)
2313, 22wcel 2139 . . . . . . . . . . . . . 14 wff 𝑦 ∈ (𝑥𝑖𝑎)
24 vb . . . . . . . . . . . . . . . . 17 setvar 𝑏
2524cv 1631 . . . . . . . . . . . . . . . 16 class 𝑏
265, 25, 9co 6813 . . . . . . . . . . . . . . 15 class (𝑥𝑖𝑏)
2715, 26wcel 2139 . . . . . . . . . . . . . 14 wff 𝑧 ∈ (𝑥𝑖𝑏)
2821, 25, 9co 6813 . . . . . . . . . . . . . . 15 class (𝑎𝑖𝑏)
297, 28wcel 2139 . . . . . . . . . . . . . 14 wff 𝑣 ∈ (𝑎𝑖𝑏)
3023, 27, 29w3a 1072 . . . . . . . . . . . . 13 wff (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))
31 vp . . . . . . . . . . . . . 14 setvar 𝑝
3231cv 1631 . . . . . . . . . . . . 13 class 𝑝
3330, 24, 32wrex 3051 . . . . . . . . . . . 12 wff 𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))
3433, 20, 32wrex 3051 . . . . . . . . . . 11 wff 𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏))
3519, 34wi 4 . . . . . . . . . 10 wff ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
3635, 6, 32wral 3050 . . . . . . . . 9 wff 𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
3736, 2, 32wral 3050 . . . . . . . 8 wff 𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
3837, 14, 32wral 3050 . . . . . . 7 wff 𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
3938, 12, 32wral 3050 . . . . . 6 wff 𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
4039, 4, 32wral 3050 . . . . 5 wff 𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
41 vf . . . . . . 7 setvar 𝑓
4241cv 1631 . . . . . 6 class 𝑓
43 citv 25534 . . . . . 6 class Itv
4442, 43cfv 6049 . . . . 5 class (Itv‘𝑓)
4540, 8, 44wsbc 3576 . . . 4 wff [(Itv‘𝑓) / 𝑖]𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
46 cbs 16059 . . . . 5 class Base
4742, 46cfv 6049 . . . 4 class (Base‘𝑓)
4845, 31, 47wsbc 3576 . . 3 wff [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))
4948, 41cab 2746 . 2 class {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))}
501, 49wceq 1632 1 wff TarskiGE = {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖]𝑥𝑝𝑦𝑝𝑧𝑝𝑢𝑝𝑣𝑝 ((𝑢 ∈ (𝑥𝑖𝑣) ∧ 𝑢 ∈ (𝑦𝑖𝑧) ∧ 𝑥𝑢) → ∃𝑎𝑝𝑏𝑝 (𝑦 ∈ (𝑥𝑖𝑎) ∧ 𝑧 ∈ (𝑥𝑖𝑏) ∧ 𝑣 ∈ (𝑎𝑖𝑏)))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkge  25555
  Copyright terms: Public domain W3C validator