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