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 30001
 Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (axtg5seg 25164). See df-ofs 31260. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.) (Modified 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 30000 . 2 class AFS
2 vg . . 3 setvar 𝑔
3 cstrkg 25129 . . 3 class TarskiG
4 ve . . . . . . . . . . . . . . . . . 18 setvar 𝑒
54cv 1474 . . . . . . . . . . . . . . . . 17 class 𝑒
6 va . . . . . . . . . . . . . . . . . . . 20 setvar 𝑎
76cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑎
8 vb . . . . . . . . . . . . . . . . . . . 20 setvar 𝑏
98cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑏
107, 9cop 4131 . . . . . . . . . . . . . . . . . 18 class 𝑎, 𝑏
11 vc . . . . . . . . . . . . . . . . . . . 20 setvar 𝑐
1211cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑐
13 vd . . . . . . . . . . . . . . . . . . . 20 setvar 𝑑
1413cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑑
1512, 14cop 4131 . . . . . . . . . . . . . . . . . 18 class 𝑐, 𝑑
1610, 15cop 4131 . . . . . . . . . . . . . . . . 17 class ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
175, 16wceq 1475 . . . . . . . . . . . . . . . 16 wff 𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
18 vf . . . . . . . . . . . . . . . . . 18 setvar 𝑓
1918cv 1474 . . . . . . . . . . . . . . . . 17 class 𝑓
20 vx . . . . . . . . . . . . . . . . . . . 20 setvar 𝑥
2120cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑥
22 vy . . . . . . . . . . . . . . . . . . . 20 setvar 𝑦
2322cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑦
2421, 23cop 4131 . . . . . . . . . . . . . . . . . 18 class 𝑥, 𝑦
25 vz . . . . . . . . . . . . . . . . . . . 20 setvar 𝑧
2625cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑧
27 vw . . . . . . . . . . . . . . . . . . . 20 setvar 𝑤
2827cv 1474 . . . . . . . . . . . . . . . . . . 19 class 𝑤
2926, 28cop 4131 . . . . . . . . . . . . . . . . . 18 class 𝑧, 𝑤
3024, 29cop 4131 . . . . . . . . . . . . . . . . 17 class ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
3119, 30wceq 1475 . . . . . . . . . . . . . . . 16 wff 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
32 vi . . . . . . . . . . . . . . . . . . . . 21 setvar 𝑖
3332cv 1474 . . . . . . . . . . . . . . . . . . . 20 class 𝑖
347, 12, 33co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑎𝑖𝑐)
359, 34wcel 1977 . . . . . . . . . . . . . . . . . 18 wff 𝑏 ∈ (𝑎𝑖𝑐)
3621, 26, 33co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑥𝑖𝑧)
3723, 36wcel 1977 . . . . . . . . . . . . . . . . . 18 wff 𝑦 ∈ (𝑥𝑖𝑧)
3835, 37wa 383 . . . . . . . . . . . . . . . . 17 wff (𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧))
39 vh . . . . . . . . . . . . . . . . . . . . 21 setvar
4039cv 1474 . . . . . . . . . . . . . . . . . . . 20 class
417, 9, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑎𝑏)
4221, 23, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑥𝑦)
4341, 42wceq 1475 . . . . . . . . . . . . . . . . . 18 wff (𝑎𝑏) = (𝑥𝑦)
449, 12, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑏𝑐)
4523, 26, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑦𝑧)
4644, 45wceq 1475 . . . . . . . . . . . . . . . . . 18 wff (𝑏𝑐) = (𝑦𝑧)
4743, 46wa 383 . . . . . . . . . . . . . . . . 17 wff ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧))
487, 14, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑎𝑑)
4921, 28, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑥𝑤)
5048, 49wceq 1475 . . . . . . . . . . . . . . . . . 18 wff (𝑎𝑑) = (𝑥𝑤)
519, 14, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑏𝑑)
5223, 28, 40co 6549 . . . . . . . . . . . . . . . . . . 19 class (𝑦𝑤)
5351, 52wceq 1475 . . . . . . . . . . . . . . . . . 18 wff (𝑏𝑑) = (𝑦𝑤)
5450, 53wa 383 . . . . . . . . . . . . . . . . 17 wff ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))
5538, 47, 54w3a 1031 . . . . . . . . . . . . . . . 16 wff ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤)))
5617, 31, 55w3a 1031 . . . . . . . . . . . . . . 15 wff (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
57 vp . . . . . . . . . . . . . . . 16 setvar 𝑝
5857cv 1474 . . . . . . . . . . . . . . 15 class 𝑝
5956, 27, 58wrex 2897 . . . . . . . . . . . . . 14 wff 𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6059, 25, 58wrex 2897 . . . . . . . . . . . . 13 wff 𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6160, 22, 58wrex 2897 . . . . . . . . . . . 12 wff 𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6261, 20, 58wrex 2897 . . . . . . . . . . 11 wff 𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6362, 13, 58wrex 2897 . . . . . . . . . 10 wff 𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6463, 11, 58wrex 2897 . . . . . . . . 9 wff 𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6564, 8, 58wrex 2897 . . . . . . . 8 wff 𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
6665, 6, 58wrex 2897 . . . . . . 7 wff 𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
672cv 1474 . . . . . . . 8 class 𝑔
68 citv 25135 . . . . . . . 8 class Itv
6967, 68cfv 5804 . . . . . . 7 class (Itv‘𝑔)
7066, 32, 69wsbc 3402 . . . . . 6 wff [(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
71 cds 15777 . . . . . . 7 class dist
7267, 71cfv 5804 . . . . . 6 class (dist‘𝑔)
7370, 39, 72wsbc 3402 . . . . 5 wff [(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
74 cbs 15695 . . . . . 6 class Base
7567, 74cfv 5804 . . . . 5 class (Base‘𝑔)
7673, 57, 75wsbc 3402 . . . 4 wff [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))
7776, 4, 18copab 4642 . . 3 class {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))}
782, 3, 77cmpt 4643 . 2 class (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))})
791, 78wceq 1475 1 wff AFS = (𝑔 ∈ TarskiG ↦ {⟨𝑒, 𝑓⟩ ∣ [(Base‘𝑔) / 𝑝][(dist‘𝑔) / ][(Itv‘𝑔) / 𝑖]𝑎𝑝𝑏𝑝𝑐𝑝𝑑𝑝𝑥𝑝𝑦𝑝𝑧𝑝𝑤𝑝 (𝑒 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑓 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 ∈ (𝑎𝑖𝑐) ∧ 𝑦 ∈ (𝑥𝑖𝑧)) ∧ ((𝑎𝑏) = (𝑥𝑦) ∧ (𝑏𝑐) = (𝑦𝑧)) ∧ ((𝑎𝑑) = (𝑥𝑤) ∧ (𝑏𝑑) = (𝑦𝑤))))})
 Colors of variables: wff setvar class This definition is referenced by:  afsval  30002
 Copyright terms: Public domain W3C validator