Metamath Proof Explorer


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

Detailed syntax breakdown

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