Metamath Proof Explorer

Theorem cshwsiun

Description: The set of (different!) words resulting by cyclically shifting a given word is an indexed union. (Contributed by AV, 19-May-2018) (Revised by AV, 8-Jun-2018) (Proof shortened by AV, 8-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m ⊢M=w∈WordV|∃n∈0..^WWcyclShiftn=w
Assertion cshwsiun ⊢W∈WordV→M=⋃n∈0..^WWcyclShiftn

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢M=w∈WordV|∃n∈0..^WWcyclShiftn=w
2 df-rab ⊢w∈WordV|∃n∈0..^WWcyclShiftn=w=w|w∈WordV∧∃n∈0..^WWcyclShiftn=w
3 eqcom ⊢WcyclShiftn=w↔w=WcyclShiftn
4 3 biimpi ⊢WcyclShiftn=w→w=WcyclShiftn
5 4 reximi ⊢∃n∈0..^WWcyclShiftn=w→∃n∈0..^Ww=WcyclShiftn
6 5 adantl ⊢w∈WordV∧∃n∈0..^WWcyclShiftn=w→∃n∈0..^Ww=WcyclShiftn
7 cshwcl ⊢W∈WordV→WcyclShiftn∈WordV
8 7 adantr ⊢W∈WordV∧n∈0..^W→WcyclShiftn∈WordV
9 eleq1 ⊢w=WcyclShiftn→w∈WordV↔WcyclShiftn∈WordV
10 8 9 syl5ibrcom ⊢W∈WordV∧n∈0..^W→w=WcyclShiftn→w∈WordV
11 10 rexlimdva ⊢W∈WordV→∃n∈0..^Ww=WcyclShiftn→w∈WordV
12 eqcom ⊢w=WcyclShiftn↔WcyclShiftn=w
13 12 biimpi ⊢w=WcyclShiftn→WcyclShiftn=w
14 13 reximi ⊢∃n∈0..^Ww=WcyclShiftn→∃n∈0..^WWcyclShiftn=w
15 11 14 jca2 ⊢W∈WordV→∃n∈0..^Ww=WcyclShiftn→w∈WordV∧∃n∈0..^WWcyclShiftn=w
16 6 15 impbid2 ⊢W∈WordV→w∈WordV∧∃n∈0..^WWcyclShiftn=w↔∃n∈0..^Ww=WcyclShiftn
17 velsn ⊢w∈WcyclShiftn↔w=WcyclShiftn
18 17 bicomi ⊢w=WcyclShiftn↔w∈WcyclShiftn
19 18 a1i ⊢W∈WordV→w=WcyclShiftn↔w∈WcyclShiftn
20 19 rexbidv ⊢W∈WordV→∃n∈0..^Ww=WcyclShiftn↔∃n∈0..^Ww∈WcyclShiftn
21 16 20 bitrd ⊢W∈WordV→w∈WordV∧∃n∈0..^WWcyclShiftn=w↔∃n∈0..^Ww∈WcyclShiftn
22 21 abbidv ⊢W∈WordV→w|w∈WordV∧∃n∈0..^WWcyclShiftn=w=w|∃n∈0..^Ww∈WcyclShiftn
23 2 22 eqtrid ⊢W∈WordV→w∈WordV|∃n∈0..^WWcyclShiftn=w=w|∃n∈0..^Ww∈WcyclShiftn
24 df-iun ⊢⋃n∈0..^WWcyclShiftn=w|∃n∈0..^Ww∈WcyclShiftn
25 23 1 24 3eqtr4g ⊢W∈WordV→M=⋃n∈0..^WWcyclShiftn