df-ifs

Description: The inner five segment configuration is an abbreviation for another congruence condition. See brifs and ifscgr for how it is used. Definition 4.1 of Schwabhauser p. 34. (Contributed by Scott Fenton, 26-Sep-2013)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cifs	$class InnerFiveSeg$
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	35 37 40	wbr	$wff ⟨a, c⟩ Cgr ⟨x, z⟩$
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, c⟩ Cgr ⟨x, z⟩ \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	22 31 40	wbr	$wff ⟨c, d⟩ Cgr ⟨z, w⟩$
50	48 49	wa	$wff (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)$
51	39 45 50	w3a	$wff ((b Btwn ⟨a, c⟩ \land y Btwn ⟨x, z⟩) \land (⟨a, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩))$
52	24 33 51	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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
53	52 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
54	53 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
55	54 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
56	55 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
57	56 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
58	57 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
59	58 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
60	59 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
61	60 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))$
62	61 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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))\}$
63	0 62	wceq	$wff InnerFiveSeg = \{⟨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, c⟩ Cgr ⟨x, z⟩ \land ⟨b, c⟩ Cgr ⟨y, z⟩) \land (⟨a, d⟩ Cgr ⟨x, w⟩ \land ⟨c, d⟩ Cgr ⟨z, w⟩)))\}$

Metamath Proof Explorer

Definition df-ifs

Detailed syntax breakdown