Definition df-segle 36794

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 36793	. 2 class Seg≤
2		vp	. . . . . . . . . . 11 setvar 𝑝
3	2	cv 1569	. . . . . . . . . 10 class 𝑝
4		va	. . . . . . . . . . . 12 setvar 𝑎
5	4	cv 1569	. . . . . . . . . . 11 class 𝑎
6		vb	. . . . . . . . . . . 12 setvar 𝑏
7	6	cv 1569	. . . . . . . . . . 11 class 𝑏
8	5, 7	cop 4589	. . . . . . . . . 10 class ⟨𝑎, 𝑏⟩
9	3, 8	wceq 1570	. . . . . . . . 9 wff 𝑝 = ⟨𝑎, 𝑏⟩
10		vq	. . . . . . . . . . 11 setvar 𝑞
11	10	cv 1569	. . . . . . . . . 10 class 𝑞
12		vc	. . . . . . . . . . . 12 setvar 𝑐
13	12	cv 1569	. . . . . . . . . . 11 class 𝑐
14		vd	. . . . . . . . . . . 12 setvar 𝑑
15	14	cv 1569	. . . . . . . . . . 11 class 𝑑
16	13, 15	cop 4589	. . . . . . . . . 10 class ⟨𝑐, 𝑑⟩
17	11, 16	wceq 1570	. . . . . . . . 9 wff 𝑞 = ⟨𝑐, 𝑑⟩
18		vy	. . . . . . . . . . . . 13 setvar 𝑦
19	18	cv 1569	. . . . . . . . . . . 12 class 𝑦
20		cbtwn 29400	. . . . . . . . . . . 12 class Btwn
21	19, 16, 20	wbr 5102	. . . . . . . . . . 11 wff 𝑦 Btwn ⟨𝑐, 𝑑⟩
22	13, 19	cop 4589	. . . . . . . . . . . 12 class ⟨𝑐, 𝑦⟩
23		ccgr 29401	. . . . . . . . . . . 12 class Cgr
24	8, 22, 23	wbr 5102	. . . . . . . . . . 11 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩
25	21, 24	wa 401	. . . . . . . . . 10 wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
26		vn	. . . . . . . . . . . 12 setvar 𝑛
27	26	cv 1569	. . . . . . . . . . 11 class 𝑛
28		cee 29399	. . . . . . . . . . 11 class 𝔼
29	27, 28	cfv 6527	. . . . . . . . . 10 class (𝔼‘𝑛)
30	25, 18, 29	wrex 3086	. . . . . . . . 9 wff ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)
31	9, 17, 30	w3a 1103	. . . . . . . 8 wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
32	31, 14, 29	wrex 3086	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
33	32, 12, 29	wrex 3086	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
34	33, 6, 29	wrex 3086	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
35	34, 4, 29	wrex 3086	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
36		cn 12305	. . . 4 class ℕ
37	35, 26, 36	wrex 3086	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))
38	37, 2, 10	copab 5166	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}
39	1, 38	wceq 1570	1 wff Seg≤ = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))}

This definition is used by:  brsegle  36795