df-ofs

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom ( ax5seg ). See brofs and 5segofs for how it is used. Definition 2.10 of Schwabhauser p. 28. (Contributed by Scott Fenton, 21-Sep-2013)

		Ref	Expression
	Assertion	df-ofs	$⊢ OuterFiveSeg = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cofs	$class OuterFiveSeg$
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		vx	$setvar x$
13		vy	$setvar y$
14		vz	$setvar z$
15		vw	$setvar w$
16	1	cv	$setvar p$
17	5	cv	$setvar a$
18	9	cv	$setvar b$
19	17 18	cop	$class ⟨a, b⟩$
20	10	cv	$setvar c$
21	11	cv	$setvar d$
22	20 21	cop	$class ⟨c, d⟩$
23	19 22	cop	$class ⟨⟨a, b⟩, ⟨c, d⟩⟩$
24	16 23	wceq	$wff p = ⟨⟨a, b⟩, ⟨c, d⟩⟩$
25	2	cv	$setvar q$
26	12	cv	$setvar x$
27	13	cv	$setvar y$
28	26 27	cop	$class ⟨x, y⟩$
29	14	cv	$setvar z$
30	15	cv	$setvar w$
31	29 30	cop	$class ⟨z, w⟩$
32	28 31	cop	$class ⟨⟨x, y⟩, ⟨z, w⟩⟩$
33	25 32	wceq	$wff q = ⟨⟨x, y⟩, ⟨z, w⟩⟩$
34		cbtwn	$class Btwn$
35	17 20	cop	$class ⟨a, c⟩$
36	18 35 34	wbr	$wff b Btwn ⟨a, c⟩$
37	26 29	cop	$class ⟨x, z⟩$
38	27 37 34	wbr	$wff y Btwn ⟨x, z⟩$
39	36 38	wa	$wff (b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩)$
40		ccgr	$class Cgr$
41	19 28 40	wbr	$wff ⟨a, b⟩ Cgr ⟨x, y⟩$
42	18 20	cop	$class ⟨b, c⟩$
43	27 29	cop	$class ⟨y, z⟩$
44	42 43 40	wbr	$wff ⟨b, c⟩ Cgr ⟨y, z⟩$
45	41 44	wa	$wff (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩)$
46	17 21	cop	$class ⟨a, d⟩$
47	26 30	cop	$class ⟨x, w⟩$
48	46 47 40	wbr	$wff ⟨a, d⟩ Cgr ⟨x, w⟩$
49	18 21	cop	$class ⟨b, d⟩$
50	27 30	cop	$class ⟨y, w⟩$
51	49 50 40	wbr	$wff ⟨b, d⟩ Cgr ⟨y, w⟩$
52	48 51	wa	$wff (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)$
53	39 45 52	w3a	$wff ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩))$
54	24 33 53	w3a	$wff (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
55	54 15 8	wrex	$wff \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
56	55 14 8	wrex	$wff \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
57	56 13 8	wrex	$wff \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
58	57 12 8	wrex	$wff \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
59	58 11 8	wrex	$wff \exists d \in 𝔼 (n) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
60	59 10 8	wrex	$wff \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
61	60 9 8	wrex	$wff \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
62	61 5 8	wrex	$wff \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
63	62 3 4	wrex	$wff \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
64	63 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) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))\}$
65	0 64	wceq	$wff OuterFiveSeg = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists x \in 𝔼 (n) \exists y \in 𝔼 (n) \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, b⟩ Cgr ⟨x, y⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))\}$

Metamath Proof Explorer

Definition df-ofs

Detailed syntax breakdown