Definition df-segle 36607

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 36606	. 2 class Seg≤
2		vp	. . . . . . . . . . 11 setvar 𝑝
3	2	cv 1568	. . . . . . . . . 10 class 𝑝
4		va	. . . . . . . . . . . 12 setvar 𝑎
5	4	cv 1568	. . . . . . . . . . 11 class 𝑎
6		vb	. . . . . . . . . . . 12 setvar 𝑏
7	6	cv 1568	. . . . . . . . . . 11 class 𝑏
8	5, 7	cop 4594	. . . . . . . . . 10 class ⟨𝑎, 𝑏⟩
9	3, 8	wceq 1569	. . . . . . . . 9 wff 𝑝 = ⟨𝑎, 𝑏⟩
10		vq	. . . . . . . . . . 11 setvar 𝑞
11	10	cv 1568	. . . . . . . . . 10 class 𝑞
12		vc	. . . . . . . . . . . 12 setvar 𝑐
13	12	cv 1568	. . . . . . . . . . 11 class 𝑐
14		vd	. . . . . . . . . . . 12 setvar 𝑑
15	14	cv 1568	. . . . . . . . . . 11 class 𝑑
16	13, 15	cop 4594	. . . . . . . . . 10 class ⟨𝑐, 𝑑⟩
17	11, 16	wceq 1569	. . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑⟩
18		vy	. . . . . . . . . . . . 13 setvar 𝑦
19	18	cv 1568	. . . . . . . . . . . 12 class 𝑦
20		cbtwn 29249	. . . . . . . . . . . 12 class Btwn
21	19, 16, 20	wbr 5108	. . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑⟩
22	13, 19	cop 4594	. . . . . . . . . . . 12 class ⟨𝑐, 𝑦⟩
23		ccgr 29250	. . . . . . . . . . . 12 class Cgr
24	8, 22, 23	wbr 5108	. . . . . . . . . . 11 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩
25	21, 24	wa 400	. . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26		vn	. . . . . . . . . . . 12 setvar 𝑛
27	26	cv 1568	. . . . . . . . . . 11 class 𝑛
28		cee 29248	. . . . . . . . . . 11 class 𝔼
29	27, 28	cfv 6536	. . . . . . . . . 10 class (𝔼‘𝑛)
30	25, 18, 29	wrex 3088	. . . . . . . . 9 wff ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
31	9, 17, 30	w3a 1102	. . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
32	31, 14, 29	wrex 3088	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
33	32, 12, 29	wrex 3088	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
34	33, 6, 29	wrex 3088	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
35	34, 4, 29	wrex 3088	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36		cn 12239	. . . 4 class ℕ
37	35, 26, 36	wrex 3088	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
38	37, 2, 10	copab 5172	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
39	1, 38	wceq 1569	1 wff Seg≤ = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}

This definition is used by:  brsegle  36608