Definition df-segle 36095

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 36094	. 2 class Seg≤
2		vp	. . . . . . . . . . 11 setvar 𝑝
3	2	cv 1539	. . . . . . . . . 10 class 𝑝
4		va	. . . . . . . . . . . 12 setvar 𝑎
5	4	cv 1539	. . . . . . . . . . 11 class 𝑎
6		vb	. . . . . . . . . . . 12 setvar 𝑏
7	6	cv 1539	. . . . . . . . . . 11 class 𝑏
8	5, 7	cop 4595	. . . . . . . . . 10 class ⟨𝑎, 𝑏⟩
9	3, 8	wceq 1540	. . . . . . . . 9 wff 𝑝 = ⟨𝑎, 𝑏⟩
10		vq	. . . . . . . . . . 11 setvar 𝑞
11	10	cv 1539	. . . . . . . . . 10 class 𝑞
12		vc	. . . . . . . . . . . 12 setvar 𝑐
13	12	cv 1539	. . . . . . . . . . 11 class 𝑐
14		vd	. . . . . . . . . . . 12 setvar 𝑑
15	14	cv 1539	. . . . . . . . . . 11 class 𝑑
16	13, 15	cop 4595	. . . . . . . . . 10 class ⟨𝑐, 𝑑⟩
17	11, 16	wceq 1540	. . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑⟩
18		vy	. . . . . . . . . . . . 13 setvar 𝑦
19	18	cv 1539	. . . . . . . . . . . 12 class 𝑦
20		cbtwn 28816	. . . . . . . . . . . 12 class Btwn
21	19, 16, 20	wbr 5107	. . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑⟩
22	13, 19	cop 4595	. . . . . . . . . . . 12 class ⟨𝑐, 𝑦⟩
23		ccgr 28817	. . . . . . . . . . . 12 class Cgr
24	8, 22, 23	wbr 5107	. . . . . . . . . . 11 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩
25	21, 24	wa 395	. . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26		vn	. . . . . . . . . . . 12 setvar 𝑛
27	26	cv 1539	. . . . . . . . . . 11 class 𝑛
28		cee 28815	. . . . . . . . . . 11 class 𝔼
29	27, 28	cfv 6511	. . . . . . . . . 10 class (𝔼‘𝑛)
30	25, 18, 29	wrex 3053	. . . . . . . . 9 wff ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
31	9, 17, 30	w3a 1086	. . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
32	31, 14, 29	wrex 3053	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
33	32, 12, 29	wrex 3053	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
34	33, 6, 29	wrex 3053	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
35	34, 4, 29	wrex 3053	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36		cn 12186	. . . 4 class ℕ
37	35, 26, 36	wrex 3053	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
38	37, 2, 10	copab 5169	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
39	1, 38	wceq 1540	1 wff Seg≤ = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}

This definition is referenced by:  brsegle  36096