Definition df-segle 34336

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

Step	Hyp	Ref	Expression
1		csegle 34335	. 2 class Seg≤
2		vp	. . . . . . . . . . 11 setvar 𝑝
3	2	cv 1538	. . . . . . . . . 10 class 𝑝
4		va	. . . . . . . . . . . 12 setvar 𝑎
5	4	cv 1538	. . . . . . . . . . 11 class 𝑎
6		vb	. . . . . . . . . . . 12 setvar 𝑏
7	6	cv 1538	. . . . . . . . . . 11 class 𝑏
8	5, 7	cop 4564	. . . . . . . . . 10 class ⟨𝑎, 𝑏⟩
9	3, 8	wceq 1539	. . . . . . . . 9 wff 𝑝 = ⟨𝑎, 𝑏⟩
10		vq	. . . . . . . . . . 11 setvar 𝑞
11	10	cv 1538	. . . . . . . . . 10 class 𝑞
12		vc	. . . . . . . . . . . 12 setvar 𝑐
13	12	cv 1538	. . . . . . . . . . 11 class 𝑐
14		vd	. . . . . . . . . . . 12 setvar 𝑑
15	14	cv 1538	. . . . . . . . . . 11 class 𝑑
16	13, 15	cop 4564	. . . . . . . . . 10 class ⟨𝑐, 𝑑⟩
17	11, 16	wceq 1539	. . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑⟩
18		vy	. . . . . . . . . . . . 13 setvar 𝑦
19	18	cv 1538	. . . . . . . . . . . 12 class 𝑦
20		cbtwn 27160	. . . . . . . . . . . 12 class Btwn
21	19, 16, 20	wbr 5070	. . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑⟩
22	13, 19	cop 4564	. . . . . . . . . . . 12 class ⟨𝑐, 𝑦⟩
23		ccgr 27161	. . . . . . . . . . . 12 class Cgr
24	8, 22, 23	wbr 5070	. . . . . . . . . . 11 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩
25	21, 24	wa 395	. . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26		vn	. . . . . . . . . . . 12 setvar 𝑛
27	26	cv 1538	. . . . . . . . . . 11 class 𝑛
28		cee 27159	. . . . . . . . . . 11 class 𝔼
29	27, 28	cfv 6418	. . . . . . . . . 10 class (𝔼‘𝑛)
30	25, 18, 29	wrex 3064	. . . . . . . . 9 wff ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
31	9, 17, 30	w3a 1085	. . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
32	31, 14, 29	wrex 3064	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
33	32, 12, 29	wrex 3064	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
34	33, 6, 29	wrex 3064	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
35	34, 4, 29	wrex 3064	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36		cn 11903	. . . 4 class ℕ
37	35, 26, 36	wrex 3064	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
38	37, 2, 10	copab 5132	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
39	1, 38	wceq 1539	1 wff Seg≤ = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}

This definition is referenced by:  brsegle  34337