df-fs

Description: The general five segment configuration is a generalization of the outer and inner five segment configurations. See brfs and fscgr for its use. Definition 4.15 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

		Ref	Expression
	Assertion	df-fs	$⊢ FiveSeg = \{⟨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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfs	$class FiveSeg$
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		ccolin	$class Colinear$
35	18 20	cop	$class ⟨b, c⟩$
36	17 35 34	wbr	$wff a Colinear ⟨b, c⟩$
37	17 35	cop	$class ⟨a, ⟨b, c⟩⟩$
38		ccgr3	$class Cgr3$
39	27 29	cop	$class ⟨y, z⟩$
40	26 39	cop	$class ⟨x, ⟨y, z⟩⟩$
41	37 40 38	wbr	$wff ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩$
42	17 21	cop	$class ⟨a, d⟩$
43		ccgr	$class Cgr$
44	26 30	cop	$class ⟨x, w⟩$
45	42 44 43	wbr	$wff ⟨a, d⟩ Cgr ⟨x, w⟩$
46	18 21	cop	$class ⟨b, d⟩$
47	27 30	cop	$class ⟨y, w⟩$
48	46 47 43	wbr	$wff ⟨b, d⟩ Cgr ⟨y, w⟩$
49	45 48	wa	$wff (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)$
50	36 41 49	w3a	$wff (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩))$
51	24 33 50	w3a	$wff (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
52	51 15 8	wrex	$wff \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
53	52 14 8	wrex	$wff \exists z \in 𝔼 (n) \exists w \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
54	53 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
55	54 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
56	55 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
57	56 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
58	57 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
59	58 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
60	59 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))$
61	60 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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))\}$
62	0 61	wceq	$wff FiveSeg = \{⟨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 (a Colinear ⟨b, c⟩ \land ⟨a, ⟨b, c⟩⟩ Cgr3 ⟨x, ⟨y, z⟩⟩ \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨b, d⟩ Cgr ⟨y, w⟩)))\}$

Metamath Proof Explorer

Definition df-fs

Detailed syntax breakdown