Definition 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 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfs	⊢ FiveSeg
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		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14		vz	⊢ 𝑧
15		vw	⊢ 𝑤
16	1	cv	⊢ 𝑝
17	5	cv	⊢ 𝑎
18	9	cv	⊢ 𝑏
19	17 18	cop	⊢ ⟨ 𝑎 , 𝑏 ⟩
20	10	cv	⊢ 𝑐
21	11	cv	⊢ 𝑑
22	20 21	cop	⊢ ⟨ 𝑐 , 𝑑 ⟩
23	19 22	cop	⊢ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩
24	16 23	wceq	⊢ 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩
25	2	cv	⊢ 𝑞
26	12	cv	⊢ 𝑥
27	13	cv	⊢ 𝑦
28	26 27	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
29	14	cv	⊢ 𝑧
30	15	cv	⊢ 𝑤
31	29 30	cop	⊢ ⟨ 𝑧 , 𝑤 ⟩
32	28 31	cop	⊢ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩
33	25 32	wceq	⊢ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩
34		ccolin	⊢ Colinear
35	18 20	cop	⊢ ⟨ 𝑏 , 𝑐 ⟩
36	17 35 34	wbr	⊢ 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩
37	17 35	cop	⊢ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩
38		ccgr3	⊢ Cgr3
39	27 29	cop	⊢ ⟨ 𝑦 , 𝑧 ⟩
40	26 39	cop	⊢ ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩
41	37 40 38	wbr	⊢ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩
42	17 21	cop	⊢ ⟨ 𝑎 , 𝑑 ⟩
43		ccgr	⊢ Cgr
44	26 30	cop	⊢ ⟨ 𝑥 , 𝑤 ⟩
45	42 44 43	wbr	⊢ ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩
46	18 21	cop	⊢ ⟨ 𝑏 , 𝑑 ⟩
47	27 30	cop	⊢ ⟨ 𝑦 , 𝑤 ⟩
48	46 47 43	wbr	⊢ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩
49	45 48	wa	⊢ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ )
50	36 41 49	w3a	⊢ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) )
51	24 33 50	w3a	⊢ ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
52	51 15 8	wrex	⊢ ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
53	52 14 8	wrex	⊢ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
54	53 13 8	wrex	⊢ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
55	54 12 8	wrex	⊢ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
56	55 11 8	wrex	⊢ ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
57	56 10 8	wrex	⊢ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
58	57 9 8	wrex	⊢ ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
59	58 5 8	wrex	⊢ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
60	59 3 4	wrex	⊢ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
61	60 1 2	copab	⊢ { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) ) }
62	0 61	wceq	⊢ FiveSeg = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( 𝑎 Colinear ⟨ 𝑏 , 𝑐 ⟩ ∧ ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ Cgr3 ⟨ 𝑥 , ⟨ 𝑦 , 𝑧 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) ) }