Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ofs Structured version   Visualization version   GIF version

Definition df-ofs 31066
Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom (ax5seg 25536). See brofs 31088 and 5segofs 31089 for how it is used. Definition 2.10 of [Schwabhauser] p. 28. (Contributed by Scott Fenton, 21-Sep-2013.)
Assertion
Ref Expression
df-ofs OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}
Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧,𝑤,𝑝,𝑞,𝑛

Detailed syntax breakdown of Definition df-ofs
StepHypRef Expression
1 cofs 31065 . 2 class OuterFiveSeg
2 vp . . . . . . . . . . . . . . 15 setvar 𝑝
32cv 1473 . . . . . . . . . . . . . 14 class 𝑝
4 va . . . . . . . . . . . . . . . . 17 setvar 𝑎
54cv 1473 . . . . . . . . . . . . . . . 16 class 𝑎
6 vb . . . . . . . . . . . . . . . . 17 setvar 𝑏
76cv 1473 . . . . . . . . . . . . . . . 16 class 𝑏
85, 7cop 4130 . . . . . . . . . . . . . . 15 class 𝑎, 𝑏
9 vc . . . . . . . . . . . . . . . . 17 setvar 𝑐
109cv 1473 . . . . . . . . . . . . . . . 16 class 𝑐
11 vd . . . . . . . . . . . . . . . . 17 setvar 𝑑
1211cv 1473 . . . . . . . . . . . . . . . 16 class 𝑑
1310, 12cop 4130 . . . . . . . . . . . . . . 15 class 𝑐, 𝑑
148, 13cop 4130 . . . . . . . . . . . . . 14 class ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
153, 14wceq 1474 . . . . . . . . . . . . 13 wff 𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩
16 vq . . . . . . . . . . . . . . 15 setvar 𝑞
1716cv 1473 . . . . . . . . . . . . . 14 class 𝑞
18 vx . . . . . . . . . . . . . . . . 17 setvar 𝑥
1918cv 1473 . . . . . . . . . . . . . . . 16 class 𝑥
20 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
2120cv 1473 . . . . . . . . . . . . . . . 16 class 𝑦
2219, 21cop 4130 . . . . . . . . . . . . . . 15 class 𝑥, 𝑦
23 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
2423cv 1473 . . . . . . . . . . . . . . . 16 class 𝑧
25 vw . . . . . . . . . . . . . . . . 17 setvar 𝑤
2625cv 1473 . . . . . . . . . . . . . . . 16 class 𝑤
2724, 26cop 4130 . . . . . . . . . . . . . . 15 class 𝑧, 𝑤
2822, 27cop 4130 . . . . . . . . . . . . . 14 class ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
2917, 28wceq 1474 . . . . . . . . . . . . 13 wff 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩
305, 10cop 4130 . . . . . . . . . . . . . . . 16 class 𝑎, 𝑐
31 cbtwn 25487 . . . . . . . . . . . . . . . 16 class Btwn
327, 30, 31wbr 4577 . . . . . . . . . . . . . . 15 wff 𝑏 Btwn ⟨𝑎, 𝑐
3319, 24cop 4130 . . . . . . . . . . . . . . . 16 class 𝑥, 𝑧
3421, 33, 31wbr 4577 . . . . . . . . . . . . . . 15 wff 𝑦 Btwn ⟨𝑥, 𝑧
3532, 34wa 382 . . . . . . . . . . . . . 14 wff (𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩)
36 ccgr 25488 . . . . . . . . . . . . . . . 16 class Cgr
378, 22, 36wbr 4577 . . . . . . . . . . . . . . 15 wff 𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦
387, 10cop 4130 . . . . . . . . . . . . . . . 16 class 𝑏, 𝑐
3921, 24cop 4130 . . . . . . . . . . . . . . . 16 class 𝑦, 𝑧
4038, 39, 36wbr 4577 . . . . . . . . . . . . . . 15 wff 𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧
4137, 40wa 382 . . . . . . . . . . . . . 14 wff (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩)
425, 12cop 4130 . . . . . . . . . . . . . . . 16 class 𝑎, 𝑑
4319, 26cop 4130 . . . . . . . . . . . . . . . 16 class 𝑥, 𝑤
4442, 43, 36wbr 4577 . . . . . . . . . . . . . . 15 wff 𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤
457, 12cop 4130 . . . . . . . . . . . . . . . 16 class 𝑏, 𝑑
4621, 26cop 4130 . . . . . . . . . . . . . . . 16 class 𝑦, 𝑤
4745, 46, 36wbr 4577 . . . . . . . . . . . . . . 15 wff 𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤
4844, 47wa 382 . . . . . . . . . . . . . 14 wff (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)
4935, 41, 48w3a 1030 . . . . . . . . . . . . 13 wff ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))
5015, 29, 49w3a 1030 . . . . . . . . . . . 12 wff (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
51 vn . . . . . . . . . . . . . 14 setvar 𝑛
5251cv 1473 . . . . . . . . . . . . 13 class 𝑛
53 cee 25486 . . . . . . . . . . . . 13 class 𝔼
5452, 53cfv 5790 . . . . . . . . . . . 12 class (𝔼‘𝑛)
5550, 25, 54wrex 2896 . . . . . . . . . . 11 wff 𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
5655, 23, 54wrex 2896 . . . . . . . . . 10 wff 𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
5756, 20, 54wrex 2896 . . . . . . . . 9 wff 𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
5857, 18, 54wrex 2896 . . . . . . . 8 wff 𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
5958, 11, 54wrex 2896 . . . . . . 7 wff 𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
6059, 9, 54wrex 2896 . . . . . 6 wff 𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
6160, 6, 54wrex 2896 . . . . 5 wff 𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
6261, 4, 54wrex 2896 . . . 4 wff 𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
63 cn 10867 . . . 4 class
6462, 51, 63wrex 2896 . . 3 wff 𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))
6564, 2, 16copab 4636 . 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}
661, 65wceq 1474 1 wff OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))}
Colors of variables: wff setvar class
This definition is referenced by:  brofs  31088
  Copyright terms: Public domain W3C validator