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 35148
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 35147 . 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 4634 . . . . . . . . . 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 4634 . . . . . . . . . 10 class 𝑐, 𝑑
1711, 16wceq 1541 . . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑
18 vy . . . . . . . . . . . . 13 setvar 𝑦
1918cv 1540 . . . . . . . . . . . 12 class 𝑦
20 cbtwn 28185 . . . . . . . . . . . 12 class Btwn
2119, 16, 20wbr 5148 . . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑
2213, 19cop 4634 . . . . . . . . . . . 12 class 𝑐, 𝑦
23 ccgr 28186 . . . . . . . . . . . 12 class Cgr
248, 22, 23wbr 5148 . . . . . . . . . . 11 wff 𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦
2521, 24wa 396 . . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26 vn . . . . . . . . . . . 12 setvar 𝑛
2726cv 1540 . . . . . . . . . . 11 class 𝑛
28 cee 28184 . . . . . . . . . . 11 class 𝔼
2927, 28cfv 6543 . . . . . . . . . 10 class (𝔼‘𝑛)
3025, 18, 29wrex 3070 . . . . . . . . 9 wff 𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
319, 17, 30w3a 1087 . . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3231, 14, 29wrex 3070 . . . . . . 7 wff 𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3332, 12, 29wrex 3070 . . . . . 6 wff 𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3433, 6, 29wrex 3070 . . . . 5 wff 𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3534, 4, 29wrex 3070 . . . 4 wff 𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36 cn 12214 . . . 4 class
3735, 26, 36wrex 3070 . . 3 wff 𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
3837, 2, 10copab 5210 . 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
391, 38wceq 1541 1 wff Seg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
Colors of variables: wff setvar class
This definition is referenced by:  brsegle  35149
  Copyright terms: Public domain W3C validator