Definition df-segle 33572

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 33571	. 2 class Seg≤
2		vp	. . . . . . . . . . 11 setvar 𝑝
3	2	cv 1535	. . . . . . . . . 10 class 𝑝
4		va	. . . . . . . . . . . 12 setvar 𝑎
5	4	cv 1535	. . . . . . . . . . 11 class 𝑎
6		vb	. . . . . . . . . . . 12 setvar 𝑏
7	6	cv 1535	. . . . . . . . . . 11 class 𝑏
8	5, 7	cop 4576	. . . . . . . . . 10 class ⟨𝑎, 𝑏⟩
9	3, 8	wceq 1536	. . . . . . . . 9 wff 𝑝 = ⟨𝑎, 𝑏⟩
10		vq	. . . . . . . . . . 11 setvar 𝑞
11	10	cv 1535	. . . . . . . . . 10 class 𝑞
12		vc	. . . . . . . . . . . 12 setvar 𝑐
13	12	cv 1535	. . . . . . . . . . 11 class 𝑐
14		vd	. . . . . . . . . . . 12 setvar 𝑑
15	14	cv 1535	. . . . . . . . . . 11 class 𝑑
16	13, 15	cop 4576	. . . . . . . . . 10 class ⟨𝑐, 𝑑⟩
17	11, 16	wceq 1536	. . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑⟩
18		vy	. . . . . . . . . . . . 13 setvar 𝑦
19	18	cv 1535	. . . . . . . . . . . 12 class 𝑦
20		cbtwn 26678	. . . . . . . . . . . 12 class Btwn
21	19, 16, 20	wbr 5069	. . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑⟩
22	13, 19	cop 4576	. . . . . . . . . . . 12 class ⟨𝑐, 𝑦⟩
23		ccgr 26679	. . . . . . . . . . . 12 class Cgr
24	8, 22, 23	wbr 5069	. . . . . . . . . . 11 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩
25	21, 24	wa 398	. . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26		vn	. . . . . . . . . . . 12 setvar 𝑛
27	26	cv 1535	. . . . . . . . . . 11 class 𝑛
28		cee 26677	. . . . . . . . . . 11 class 𝔼
29	27, 28	cfv 6358	. . . . . . . . . 10 class (𝔼‘𝑛)
30	25, 18, 29	wrex 3142	. . . . . . . . 9 wff ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
31	9, 17, 30	w3a 1083	. . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
32	31, 14, 29	wrex 3142	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
33	32, 12, 29	wrex 3142	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
34	33, 6, 29	wrex 3142	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
35	34, 4, 29	wrex 3142	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36		cn 11641	. . . 4 class ℕ
37	35, 26, 36	wrex 3142	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
38	37, 2, 10	copab 5131	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
39	1, 38	wceq 1536	1 wff Seg≤ = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}

This definition is referenced by:  brsegle  33573