Definition df-segle

Description: Define the segment length comparison relationship. This relationship expresses that the segment A B is no longer than C D . 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)

	Ref	Expression
Assertion	df-segle	⊢ Seg≤ = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) }

Detailed syntax breakdown

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