Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trkg2d Structured version   Visualization version   GIF version

Definition df-trkg2d 33976
Description: Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of [Schwabhauser] p. 12, and the upper dimension axiom, Axiom A9 of [Schwabhauser] p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019.) (New usage is discouraged.)
Assertion
Ref Expression
df-trkg2d TarskiG2D = {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(distβ€˜π‘“) / 𝑑][(Itvβ€˜π‘“) / 𝑖](βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))}
Distinct variable group:   𝑓,𝑑,𝑖,𝑝,𝑒,𝑣,π‘₯,𝑦,𝑧

Detailed syntax breakdown of Definition df-trkg2d
StepHypRef Expression
1 cstrkg2d 33975 . 2 class TarskiG2D
2 vz . . . . . . . . . . . . . 14 setvar 𝑧
32cv 1539 . . . . . . . . . . . . 13 class 𝑧
4 vx . . . . . . . . . . . . . . 15 setvar π‘₯
54cv 1539 . . . . . . . . . . . . . 14 class π‘₯
6 vy . . . . . . . . . . . . . . 15 setvar 𝑦
76cv 1539 . . . . . . . . . . . . . 14 class 𝑦
8 vi . . . . . . . . . . . . . . 15 setvar 𝑖
98cv 1539 . . . . . . . . . . . . . 14 class 𝑖
105, 7, 9co 7412 . . . . . . . . . . . . 13 class (π‘₯𝑖𝑦)
113, 10wcel 2105 . . . . . . . . . . . 12 wff 𝑧 ∈ (π‘₯𝑖𝑦)
123, 7, 9co 7412 . . . . . . . . . . . . 13 class (𝑧𝑖𝑦)
135, 12wcel 2105 . . . . . . . . . . . 12 wff π‘₯ ∈ (𝑧𝑖𝑦)
145, 3, 9co 7412 . . . . . . . . . . . . 13 class (π‘₯𝑖𝑧)
157, 14wcel 2105 . . . . . . . . . . . 12 wff 𝑦 ∈ (π‘₯𝑖𝑧)
1611, 13, 15w3o 1085 . . . . . . . . . . 11 wff (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
1716wn 3 . . . . . . . . . 10 wff Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
18 vp . . . . . . . . . . 11 setvar 𝑝
1918cv 1539 . . . . . . . . . 10 class 𝑝
2017, 2, 19wrex 3069 . . . . . . . . 9 wff βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
2120, 6, 19wrex 3069 . . . . . . . 8 wff βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
2221, 4, 19wrex 3069 . . . . . . 7 wff βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))
23 vu . . . . . . . . . . . . . . . . . 18 setvar 𝑒
2423cv 1539 . . . . . . . . . . . . . . . . 17 class 𝑒
25 vd . . . . . . . . . . . . . . . . . 18 setvar 𝑑
2625cv 1539 . . . . . . . . . . . . . . . . 17 class 𝑑
275, 24, 26co 7412 . . . . . . . . . . . . . . . 16 class (π‘₯𝑑𝑒)
28 vv . . . . . . . . . . . . . . . . . 18 setvar 𝑣
2928cv 1539 . . . . . . . . . . . . . . . . 17 class 𝑣
305, 29, 26co 7412 . . . . . . . . . . . . . . . 16 class (π‘₯𝑑𝑣)
3127, 30wceq 1540 . . . . . . . . . . . . . . 15 wff (π‘₯𝑑𝑒) = (π‘₯𝑑𝑣)
327, 24, 26co 7412 . . . . . . . . . . . . . . . 16 class (𝑦𝑑𝑒)
337, 29, 26co 7412 . . . . . . . . . . . . . . . 16 class (𝑦𝑑𝑣)
3432, 33wceq 1540 . . . . . . . . . . . . . . 15 wff (𝑦𝑑𝑒) = (𝑦𝑑𝑣)
353, 24, 26co 7412 . . . . . . . . . . . . . . . 16 class (𝑧𝑑𝑒)
363, 29, 26co 7412 . . . . . . . . . . . . . . . 16 class (𝑧𝑑𝑣)
3735, 36wceq 1540 . . . . . . . . . . . . . . 15 wff (𝑧𝑑𝑒) = (𝑧𝑑𝑣)
3831, 34, 37w3a 1086 . . . . . . . . . . . . . 14 wff ((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣))
3924, 29wne 2939 . . . . . . . . . . . . . 14 wff 𝑒 β‰  𝑣
4038, 39wa 395 . . . . . . . . . . . . 13 wff (((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣)
4140, 16wi 4 . . . . . . . . . . . 12 wff ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4241, 28, 19wral 3060 . . . . . . . . . . 11 wff βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4342, 23, 19wral 3060 . . . . . . . . . 10 wff βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4443, 2, 19wral 3060 . . . . . . . . 9 wff βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4544, 6, 19wral 3060 . . . . . . . 8 wff βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4645, 4, 19wral 3060 . . . . . . 7 wff βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)))
4722, 46wa 395 . . . . . 6 wff (βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
48 vf . . . . . . . 8 setvar 𝑓
4948cv 1539 . . . . . . 7 class 𝑓
50 citv 27952 . . . . . . 7 class Itv
5149, 50cfv 6543 . . . . . 6 class (Itvβ€˜π‘“)
5247, 8, 51wsbc 3777 . . . . 5 wff [(Itvβ€˜π‘“) / 𝑖](βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
53 cds 17211 . . . . . 6 class dist
5449, 53cfv 6543 . . . . 5 class (distβ€˜π‘“)
5552, 25, 54wsbc 3777 . . . 4 wff [(distβ€˜π‘“) / 𝑑][(Itvβ€˜π‘“) / 𝑖](βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
56 cbs 17149 . . . . 5 class Base
5749, 56cfv 6543 . . . 4 class (Baseβ€˜π‘“)
5855, 18, 57wsbc 3777 . . 3 wff [(Baseβ€˜π‘“) / 𝑝][(distβ€˜π‘“) / 𝑑][(Itvβ€˜π‘“) / 𝑖](βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))
5958, 48cab 2708 . 2 class {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(distβ€˜π‘“) / 𝑑][(Itvβ€˜π‘“) / 𝑖](βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))}
601, 59wceq 1540 1 wff TarskiG2D = {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(distβ€˜π‘“) / 𝑑][(Itvβ€˜π‘“) / 𝑖](βˆƒπ‘₯ ∈ 𝑝 βˆƒπ‘¦ ∈ 𝑝 βˆƒπ‘§ ∈ 𝑝 Β¬ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧)) ∧ βˆ€π‘₯ ∈ 𝑝 βˆ€π‘¦ ∈ 𝑝 βˆ€π‘§ ∈ 𝑝 βˆ€π‘’ ∈ 𝑝 βˆ€π‘£ ∈ 𝑝 ((((π‘₯𝑑𝑒) = (π‘₯𝑑𝑣) ∧ (𝑦𝑑𝑒) = (𝑦𝑑𝑣) ∧ (𝑧𝑑𝑒) = (𝑧𝑑𝑣)) ∧ 𝑒 β‰  𝑣) β†’ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))))}
Colors of variables: wff setvar class
This definition is referenced by:  istrkg2d  33977
  Copyright terms: Public domain W3C validator