Metamath Proof Explorer


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 ⟨ 𝑦 , 𝑤 ⟩ ) ) ) }