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}_{\leq} = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csegle	$class {Seg}_{\leq}$
1		vp	$setvar p$
2		vq	$setvar q$
3		vn	$setvar n$
4		cn	$class ℕ$
5		va	$setvar a$
6		cee	$class 𝔼$
7	3	cv	$setvar n$
8	7 6	cfv	$class 𝔼 (n)$
9		vb	$setvar b$
10		vc	$setvar c$
11		vd	$setvar d$
12	1	cv	$setvar p$
13	5	cv	$setvar a$
14	9	cv	$setvar b$
15	13 14	cop	$class ⟨a, b⟩$
16	12 15	wceq	$wff p = ⟨a, b⟩$
17	2	cv	$setvar q$
18	10	cv	$setvar c$
19	11	cv	$setvar d$
20	18 19	cop	$class ⟨c, d⟩$
21	17 20	wceq	$wff q = ⟨c, d⟩$
22		vy	$setvar y$
23	22	cv	$setvar y$
24		cbtwn	$class Btwn$
25	23 20 24	wbr	$wff y Btwn ⟨c, d⟩$
26		ccgr	$class Cgr$
27	18 23	cop	$class ⟨c, y⟩$
28	15 27 26	wbr	$wff ⟨a, b⟩ Cgr ⟨c, y⟩$
29	25 28	wa	$wff (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)$
30	29 22 8	wrex	$wff \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)$
31	16 21 30	w3a	$wff (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
32	31 11 8	wrex	$wff \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
33	32 10 8	wrex	$wff \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
34	33 9 8	wrex	$wff \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
35	34 5 8	wrex	$wff \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
36	35 3 4	wrex	$wff \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
37	36 1 2	copab	$class \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))\}$
38	0 37	wceq	$wff {Seg}_{\leq} = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))\}$

Metamath Proof Explorer

Definition df-segle

Detailed syntax breakdown