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 33628
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 33627 . 2 class Seg
2 vp . . . . . . . . . . 11 setvar 𝑝
32cv 1537 . . . . . . . . . 10 class 𝑝
4 va . . . . . . . . . . . 12 setvar 𝑎
54cv 1537 . . . . . . . . . . 11 class 𝑎
6 vb . . . . . . . . . . . 12 setvar 𝑏
76cv 1537 . . . . . . . . . . 11 class 𝑏
85, 7cop 4557 . . . . . . . . . 10 class 𝑎, 𝑏
93, 8wceq 1538 . . . . . . . . 9 wff 𝑝 = ⟨𝑎, 𝑏
10 vq . . . . . . . . . . 11 setvar 𝑞
1110cv 1537 . . . . . . . . . 10 class 𝑞
12 vc . . . . . . . . . . . 12 setvar 𝑐
1312cv 1537 . . . . . . . . . . 11 class 𝑐
14 vd . . . . . . . . . . . 12 setvar 𝑑
1514cv 1537 . . . . . . . . . . 11 class 𝑑
1613, 15cop 4557 . . . . . . . . . 10 class 𝑐, 𝑑
1711, 16wceq 1538 . . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑
18 vy . . . . . . . . . . . . 13 setvar 𝑦
1918cv 1537 . . . . . . . . . . . 12 class 𝑦
20 cbtwn 26689 . . . . . . . . . . . 12 class Btwn
2119, 16, 20wbr 5053 . . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑
2213, 19cop 4557 . . . . . . . . . . . 12 class 𝑐, 𝑦
23 ccgr 26690 . . . . . . . . . . . 12 class Cgr
248, 22, 23wbr 5053 . . . . . . . . . . 11 wff 𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦
2521, 24wa 399 . . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26 vn . . . . . . . . . . . 12 setvar 𝑛
2726cv 1537 . . . . . . . . . . 11 class 𝑛
28 cee 26688 . . . . . . . . . . 11 class 𝔼
2927, 28cfv 6344 . . . . . . . . . 10 class (𝔼‘𝑛)
3025, 18, 29wrex 3134 . . . . . . . . 9 wff 𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
319, 17, 30w3a 1084 . . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3231, 14, 29wrex 3134 . . . . . . 7 wff 𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3332, 12, 29wrex 3134 . . . . . 6 wff 𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3433, 6, 29wrex 3134 . . . . 5 wff 𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3534, 4, 29wrex 3134 . . . 4 wff 𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36 cn 11637 . . . 4 class
3735, 26, 36wrex 3134 . . 3 wff 𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3837, 2, 10copab 5115 . 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
391, 38wceq 1538 1 wff Seg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
Colors of variables: wff setvar class
This definition is referenced by:  brsegle  33629
  Copyright terms: Public domain W3C validator