Theorem tocycval

Description: Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023)

	Ref	Expression
Hypothesis	tocycval.1	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
Assertion	tocycval	⊢ ( 𝐷 ∈ 𝑉 → 𝐶 = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tocycval.1	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2		df-tocyc	⊢ toCyc = ( 𝑑 ∈ V ↦ ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )
3		wrdeq	⊢ ( 𝑑 = 𝐷 → Word 𝑑 = Word 𝐷 )
4		f1eq3	⊢ ( 𝑑 = 𝐷 → ( 𝑢 : dom 𝑢 –1-1→ 𝑑 ↔ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
5	3 4	rabeqbidv	⊢ ( 𝑑 = 𝐷 → { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } = { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } )
6		difeq1	⊢ ( 𝑑 = 𝐷 → ( 𝑑 ∖ ran 𝑤 ) = ( 𝐷 ∖ ran 𝑤 ) )
7	6	reseq2d	⊢ ( 𝑑 = 𝐷 → ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) = ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) )
8	7	uneq1d	⊢ ( 𝑑 = 𝐷 → ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) )
9	5 8	mpteq12dv	⊢ ( 𝑑 = 𝐷 → ( 𝑤 ∈ { 𝑢 ∈ Word 𝑑 ∣ 𝑢 : dom 𝑢 –1-1→ 𝑑 } ↦ ( ( I ↾ ( 𝑑 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )
10		elex	⊢ ( 𝐷 ∈ 𝑉 → 𝐷 ∈ V )
11		eqid	⊢ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } = { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 }
12		wrdexg	⊢ ( 𝐷 ∈ 𝑉 → Word 𝐷 ∈ V )
13	11 12	rabexd	⊢ ( 𝐷 ∈ 𝑉 → { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ∈ V )
14	13	mptexd	⊢ ( 𝐷 ∈ 𝑉 → ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) ∈ V )
15	2 9 10 14	fvmptd3	⊢ ( 𝐷 ∈ 𝑉 → ( toCyc ‘ 𝐷 ) = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )
16	1 15	eqtrid	⊢ ( 𝐷 ∈ 𝑉 → 𝐶 = ( 𝑤 ∈ { 𝑢 ∈ Word 𝐷 ∣ 𝑢 : dom 𝑢 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑤 ) ) ∪ ( ( 𝑤 cyclShift 1 ) ∘ ◡ 𝑤 ) ) ) )