# Metamath Proof Explorer

## Theorem cshwrepswhash1

Description: The size of the set of (different!) words resulting by cyclically shifting a nonempty "repeated symbol word" is 1. (Contributed by AV, 18-May-2018) (Revised by AV, 8-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
Assertion cshwrepswhash1 ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( ♯ ‘ 𝑀 ) = 1 )

### Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
2 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3 repsdf2 ( ( 𝐴𝑉𝑁 ∈ ℕ0 ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) ) )
4 2 3 sylan2 ( ( 𝐴𝑉𝑁 ∈ ℕ ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) ) )
5 simp1 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) → 𝑊 ∈ Word 𝑉 )
6 5 adantl ( ( ( 𝐴𝑉𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) ) → 𝑊 ∈ Word 𝑉 )
7 eleq1 ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
8 7 eqcoms ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
9 lbfzo0 ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ )
10 9 biimpri ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
11 8 10 syl6bi ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
12 11 3ad2ant2 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) → ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
13 12 com12 ( 𝑁 ∈ ℕ → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
14 13 adantl ( ( 𝐴𝑉𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
15 14 imp ( ( ( 𝐴𝑉𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
16 cshw0 ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 0 ) = 𝑊 )
17 6 16 syl ( ( ( 𝐴𝑉𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) ) → ( 𝑊 cyclShift 0 ) = 𝑊 )
18 oveq2 ( 𝑛 = 0 → ( 𝑊 cyclShift 𝑛 ) = ( 𝑊 cyclShift 0 ) )
19 18 eqeq1d ( 𝑛 = 0 → ( ( 𝑊 cyclShift 𝑛 ) = 𝑊 ↔ ( 𝑊 cyclShift 0 ) = 𝑊 ) )
20 19 rspcev ( ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 0 ) = 𝑊 ) → ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 )
21 15 17 20 syl2anc ( ( ( 𝐴𝑉𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) ) → ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 )
22 eqeq2 ( 𝑤 = 𝑊 → ( ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ( 𝑊 cyclShift 𝑛 ) = 𝑊 ) )
23 22 rexbidv ( 𝑤 = 𝑊 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 ) )
24 23 rspcev ( ( 𝑊 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑊 ) → ∃ 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
25 6 21 24 syl2anc ( ( ( 𝐴𝑉𝑁 ∈ ℕ ) ∧ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) ) → ∃ 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
26 25 ex ( ( 𝐴𝑉𝑁 ∈ ℕ ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) → ∃ 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) )
27 4 26 sylbid ( ( 𝐴𝑉𝑁 ∈ ℕ ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) → ∃ 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) )
28 27 3impia ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
29 repsw ( ( 𝐴𝑉𝑁 ∈ ℕ0 ) → ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 )
30 2 29 sylan2 ( ( 𝐴𝑉𝑁 ∈ ℕ ) → ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 )
31 30 3adant3 ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 )
32 simpll3 ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 = ( 𝐴 repeatS 𝑁 ) )
33 32 oveq1d ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑛 ) = ( ( 𝐴 repeatS 𝑁 ) cyclShift 𝑛 ) )
34 simp1 ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → 𝐴𝑉 )
35 34 ad2antrr ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐴𝑉 )
36 2 3ad2ant2 ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → 𝑁 ∈ ℕ0 )
37 36 ad2antrr ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑁 ∈ ℕ0 )
38 elfzoelz ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → 𝑛 ∈ ℤ )
39 38 adantl ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑛 ∈ ℤ )
40 repswcshw ( ( 𝐴𝑉𝑁 ∈ ℕ0𝑛 ∈ ℤ ) → ( ( 𝐴 repeatS 𝑁 ) cyclShift 𝑛 ) = ( 𝐴 repeatS 𝑁 ) )
41 35 37 39 40 syl3anc ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝐴 repeatS 𝑁 ) cyclShift 𝑛 ) = ( 𝐴 repeatS 𝑁 ) )
42 33 41 eqtrd ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑛 ) = ( 𝐴 repeatS 𝑁 ) )
43 42 eqeq1d ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑛 ) = 𝑢 ↔ ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
44 43 biimpd ( ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
45 44 rexlimdva ( ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) ∧ 𝑢 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
46 45 ralrimiva ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
47 eqeq1 ( 𝑤 = ( 𝐴 repeatS 𝑁 ) → ( 𝑤 = 𝑢 ↔ ( 𝐴 repeatS 𝑁 ) = 𝑢 ) )
48 47 imbi2d ( 𝑤 = ( 𝐴 repeatS 𝑁 ) → ( ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢𝑤 = 𝑢 ) ↔ ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) ) )
49 48 ralbidv ( 𝑤 = ( 𝐴 repeatS 𝑁 ) → ( ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢𝑤 = 𝑢 ) ↔ ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) ) )
50 49 rspcev ( ( ( 𝐴 repeatS 𝑁 ) ∈ Word 𝑉 ∧ ∀ 𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 → ( 𝐴 repeatS 𝑁 ) = 𝑢 ) ) → ∃ 𝑤 ∈ Word 𝑉𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢𝑤 = 𝑢 ) )
51 31 46 50 syl2anc ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑤 ∈ Word 𝑉𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢𝑤 = 𝑢 ) )
52 eqeq2 ( 𝑤 = 𝑢 → ( ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ( 𝑊 cyclShift 𝑛 ) = 𝑢 ) )
53 52 rexbidv ( 𝑤 = 𝑢 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢 ) )
54 53 reu7 ( ∃! 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ( ∃ 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ∧ ∃ 𝑤 ∈ Word 𝑉𝑢 ∈ Word 𝑉 ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑢𝑤 = 𝑢 ) ) )
55 28 51 54 sylanbrc ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃! 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
56 reusn ( ∃! 𝑤 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑟 { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
57 55 56 sylib ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑟 { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
58 1 eqeq1i ( 𝑀 = { 𝑟 } ↔ { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
59 58 exbii ( ∃ 𝑟 𝑀 = { 𝑟 } ↔ ∃ 𝑟 { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑟 } )
60 57 59 sylibr ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ∃ 𝑟 𝑀 = { 𝑟 } )
61 1 cshwsex ( 𝑊 ∈ Word 𝑉𝑀 ∈ V )
62 61 3ad2ant1 ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊𝑖 ) = 𝐴 ) → 𝑀 ∈ V )
63 4 62 syl6bi ( ( 𝐴𝑉𝑁 ∈ ℕ ) → ( 𝑊 = ( 𝐴 repeatS 𝑁 ) → 𝑀 ∈ V ) )
64 63 3impia ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → 𝑀 ∈ V )
65 hash1snb ( 𝑀 ∈ V → ( ( ♯ ‘ 𝑀 ) = 1 ↔ ∃ 𝑟 𝑀 = { 𝑟 } ) )
66 64 65 syl ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( ( ♯ ‘ 𝑀 ) = 1 ↔ ∃ 𝑟 𝑀 = { 𝑟 } ) )
67 60 66 mpbird ( ( 𝐴𝑉𝑁 ∈ ℕ ∧ 𝑊 = ( 𝐴 repeatS 𝑁 ) ) → ( ♯ ‘ 𝑀 ) = 1 )