Theorem cshwsexa

Description: The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by AV, 8-Jun-2018) (Revised by Mario Carneiro/AV, 25-Oct-2018) (Proof shortened by SN, 15-Jan-2025)

	Ref	Expression
Assertion	cshwsexa	⊢ { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
2	1	rexbii	⊢ ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
3	2	abbii	⊢ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) }
4		ovex	⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ V
5	4	abrexex	⊢ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) } ∈ V
6	3 5	eqeltri	⊢ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ∈ V
7		rabssab	⊢ { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ⊆ { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
8	6 7	ssexi	⊢ { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } ∈ V