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