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

Definition df-afs 32220
Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 26411). See df-ofs 33928. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) (Revised by Thierry Arnoux, 15-Mar-2019.)
Assertion
Ref Expression
df-afs AFS = (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))})
Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧,𝑤,𝑒,𝑓,𝑔,,𝑖,𝑝

Detailed syntax breakdown of Definition df-afs
StepHypRef Expression
1 cafs 32219 . 2 class AFS
2 vg . . 3 setvar 𝑔
3 cstrkg 26376 . . 3 class TarskiG
4 ve . . . . . . . . . . . . . . . . . 18 setvar 𝑒
54cv 1541 . . . . . . . . . . . . . . . . 17 class 𝑒
6 va . . . . . . . . . . . . . . . . . . . 20 setvar 𝑎
76cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑎
8 vb . . . . . . . . . . . . . . . . . . . 20 setvar 𝑏
98cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑏
107, 9cop 4522 . . . . . . . . . . . . . . . . . 18 class 𝑎, 𝑏
11 vc . . . . . . . . . . . . . . . . . . . 20 setvar 𝑐
1211cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑐
13 vd . . . . . . . . . . . . . . . . . . . 20 setvar 𝑑
1413cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑑
1512, 14cop 4522 . . . . . . . . . . . . . . . . . 18 class 𝑐, 𝑑
1610, 15cop 4522 . . . . . . . . . . . . . . . . 17 class ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
175, 16wceq 1542 . . . . . . . . . . . . . . . 16 wff 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
18 vf . . . . . . . . . . . . . . . . . 18 setvar 𝑓
1918cv 1541 . . . . . . . . . . . . . . . . 17 class 𝑓
20 vx . . . . . . . . . . . . . . . . . . . 20 setvar 𝑥
2120cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑥
22 vy . . . . . . . . . . . . . . . . . . . 20 setvar 𝑦
2322cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑦
2421, 23cop 4522 . . . . . . . . . . . . . . . . . 18 class 𝑥, 𝑦
25 vz . . . . . . . . . . . . . . . . . . . 20 setvar 𝑧
2625cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑧
27 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
2827cv 1541 . . . . . . . . . . . . . . . . . . 19 class 𝑤
2926, 28cop 4522 . . . . . . . . . . . . . . . . . 18 class 𝑧, 𝑤
3024, 29cop 4522 . . . . . . . . . . . . . . . . 17 class ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
3119, 30wceq 1542 . . . . . . . . . . . . . . . 16 wff 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
32 vi . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑖
3332cv 1541 . . . . . . . . . . . . . . . . . . . 20 class 𝑖
347, 12, 33co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑎𝑖𝑐)
359, 34wcel 2114 . . . . . . . . . . . . . . . . . 18 wff 𝑏 ∈ (𝑎𝑖𝑐)
3621, 26, 33co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑥𝑖𝑧)
3723, 36wcel 2114 . . . . . . . . . . . . . . . . . 18 wff 𝑦 ∈ (𝑥𝑖𝑧)
3835, 37wa 399 . . . . . . . . . . . . . . . . 17 wff (𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧))
39 vh . . . . . . . . . . . . . . . . . . . . 21 setvar
4039cv 1541 . . . . . . . . . . . . . . . . . . . 20 class
417, 9, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑎𝑏)
4221, 23, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑥𝑦)
4341, 42wceq 1542 . . . . . . . . . . . . . . . . . 18 wff (𝑎𝑏) = (𝑥𝑦)
449, 12, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑏𝑐)
4523, 26, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑦𝑧)
4644, 45wceq 1542 . . . . . . . . . . . . . . . . . 18 wff (𝑏𝑐) = (𝑦𝑧)
4743, 46wa 399 . . . . . . . . . . . . . . . . 17 wff ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧))
487, 14, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑎𝑑)
4921, 28, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑥𝑤)
5048, 49wceq 1542 . . . . . . . . . . . . . . . . . 18 wff (𝑎𝑑) = (𝑥𝑤)
519, 14, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑏𝑑)
5223, 28, 40co 7170 . . . . . . . . . . . . . . . . . . 19 class (𝑦𝑤)
5351, 52wceq 1542 . . . . . . . . . . . . . . . . . 18 wff (𝑏𝑑) = (𝑦𝑤)
5450, 53wa 399 . . . . . . . . . . . . . . . . 17 wff ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))
5538, 47, 54w3a 1088 . . . . . . . . . . . . . . . 16 wff ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))
5617, 31, 55w3a 1088 . . . . . . . . . . . . . . 15 wff (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
57 vp . . . . . . . . . . . . . . . 16 setvar 𝑝
5857cv 1541 . . . . . . . . . . . . . . 15 class 𝑝
5956, 27, 58wrex 3054 . . . . . . . . . . . . . 14 wff 𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6059, 25, 58wrex 3054 . . . . . . . . . . . . 13 wff 𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6160, 22, 58wrex 3054 . . . . . . . . . . . 12 wff 𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6261, 20, 58wrex 3054 . . . . . . . . . . 11 wff 𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6362, 13, 58wrex 3054 . . . . . . . . . 10 wff 𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6463, 11, 58wrex 3054 . . . . . . . . 9 wff 𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6564, 8, 58wrex 3054 . . . . . . . 8 wff 𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6665, 6, 58wrex 3054 . . . . . . 7 wff 𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
672cv 1541 . . . . . . . 8 class 𝑔
68 citv 26382 . . . . . . . 8 class Itv
6967, 68cfv 6339 . . . . . . 7 class (Itv‘𝑔)
7066, 32, 69wsbc 3680 . . . . . 6 wff [(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
71 cds 16677 . . . . . . 7 class dist
7267, 71cfv 6339 . . . . . 6 class (dist‘𝑔)
7370, 39, 72wsbc 3680 . . . . 5 wff [(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
74 cbs 16586 . . . . . 6 class Base
7567, 74cfv 6339 . . . . 5 class (Base‘𝑔)
7673, 57, 75wsbc 3680 . . . 4 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
7776, 4, 18copab 5092 . . 3 class {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))}
782, 3, 77cmpt 5110 . 2 class (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))})
791, 78wceq 1542 1 wff AFS = (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))})
Colors of variables: wff setvar class
This definition is referenced by:  afsval  32221
  Copyright terms: Public domain W3C validator