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

Definition df-segle 32540
Description: Define the segment length comparison relationship. This relationship expresses that the segment 𝐴𝐵 is no longer than 𝐶𝐷. In this section, we establish various properties of this relationship showing that it is a transitive, reflexive relationship on pairs of points that is substitutive under congruence. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Scott Fenton, 11-Oct-2013.)
Assertion
Ref Expression
df-segle Seg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
Distinct variable group:   𝑞,𝑝,𝑛,𝑎,𝑏,𝑐,𝑑,𝑦

Detailed syntax breakdown of Definition df-segle
StepHypRef Expression
1 csegle 32539 . 2 class Seg
2 vp . . . . . . . . . . 11 setvar 𝑝
32cv 1636 . . . . . . . . . 10 class 𝑝
4 va . . . . . . . . . . . 12 setvar 𝑎
54cv 1636 . . . . . . . . . . 11 class 𝑎
6 vb . . . . . . . . . . . 12 setvar 𝑏
76cv 1636 . . . . . . . . . . 11 class 𝑏
85, 7cop 4383 . . . . . . . . . 10 class 𝑎, 𝑏
93, 8wceq 1637 . . . . . . . . 9 wff 𝑝 = ⟨𝑎, 𝑏
10 vq . . . . . . . . . . 11 setvar 𝑞
1110cv 1636 . . . . . . . . . 10 class 𝑞
12 vc . . . . . . . . . . . 12 setvar 𝑐
1312cv 1636 . . . . . . . . . . 11 class 𝑐
14 vd . . . . . . . . . . . 12 setvar 𝑑
1514cv 1636 . . . . . . . . . . 11 class 𝑑
1613, 15cop 4383 . . . . . . . . . 10 class 𝑐, 𝑑
1711, 16wceq 1637 . . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑
18 vy . . . . . . . . . . . . 13 setvar 𝑦
1918cv 1636 . . . . . . . . . . . 12 class 𝑦
20 cbtwn 25989 . . . . . . . . . . . 12 class Btwn
2119, 16, 20wbr 4851 . . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑
2213, 19cop 4383 . . . . . . . . . . . 12 class 𝑐, 𝑦
23 ccgr 25990 . . . . . . . . . . . 12 class Cgr
248, 22, 23wbr 4851 . . . . . . . . . . 11 wff 𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦
2521, 24wa 384 . . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26 vn . . . . . . . . . . . 12 setvar 𝑛
2726cv 1636 . . . . . . . . . . 11 class 𝑛
28 cee 25988 . . . . . . . . . . 11 class 𝔼
2927, 28cfv 6104 . . . . . . . . . 10 class (𝔼‘𝑛)
3025, 18, 29wrex 3104 . . . . . . . . 9 wff 𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
319, 17, 30w3a 1100 . . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3231, 14, 29wrex 3104 . . . . . . 7 wff 𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3332, 12, 29wrex 3104 . . . . . 6 wff 𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3433, 6, 29wrex 3104 . . . . 5 wff 𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3534, 4, 29wrex 3104 . . . 4 wff 𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36 cn 11308 . . . 4 class
3735, 26, 36wrex 3104 . . 3 wff 𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3837, 2, 10copab 4913 . 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
391, 38wceq 1637 1 wff Seg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
Colors of variables: wff setvar class
This definition is referenced by:  brsegle  32541
  Copyright terms: Public domain W3C validator