Metamath Proof Explorer

Theorem tocycval

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

Ref Expression
Hypothesis tocycval.1 ⊢C=toCyc⁡D
Assertion tocycval ⊢D∈V→C=w∈u∈WordD|u:dom⁡u⟶1-1D⟼I↾D∖ran⁡w∪wcyclShift1∘w-1

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢C=toCyc⁡D
2 df-tocyc ⊢toCyc=d∈V⟼w∈u∈Wordd|u:dom⁡u⟶1-1d⟼I↾d∖ran⁡w∪wcyclShift1∘w-1
3 wrdeq ⊢d=D→Wordd=WordD
4 f1eq3 ⊢d=D→u:dom⁡u⟶1-1d↔u:dom⁡u⟶1-1D
5 3 4 rabeqbidv ⊢d=D→u∈Wordd|u:dom⁡u⟶1-1d=u∈WordD|u:dom⁡u⟶1-1D
6 difeq1 ⊢d=D→d∖ran⁡w=D∖ran⁡w
7 6 reseq2d ⊢d=D→I↾d∖ran⁡w=I↾D∖ran⁡w
8 7 uneq1d ⊢d=D→I↾d∖ran⁡w∪wcyclShift1∘w-1=I↾D∖ran⁡w∪wcyclShift1∘w-1
9 5 8 mpteq12dv ⊢d=D→w∈u∈Wordd|u:dom⁡u⟶1-1d⟼I↾d∖ran⁡w∪wcyclShift1∘w-1=w∈u∈WordD|u:dom⁡u⟶1-1D⟼I↾D∖ran⁡w∪wcyclShift1∘w-1
10 elex ⊢D∈V→D∈V
11 eqid ⊢u∈WordD|u:dom⁡u⟶1-1D=u∈WordD|u:dom⁡u⟶1-1D
12 wrdexg ⊢D∈V→WordD∈V
13 11 12 rabexd ⊢D∈V→u∈WordD|u:dom⁡u⟶1-1D∈V
14 13 mptexd ⊢D∈V→w∈u∈WordD|u:dom⁡u⟶1-1D⟼I↾D∖ran⁡w∪wcyclShift1∘w-1∈V
15 2 9 10 14 fvmptd3 ⊢D∈V→toCyc⁡D=w∈u∈WordD|u:dom⁡u⟶1-1D⟼I↾D∖ran⁡w∪wcyclShift1∘w-1
16 1 15 eqtrid ⊢D∈V→C=w∈u∈WordD|u:dom⁡u⟶1-1D⟼I↾D∖ran⁡w∪wcyclShift1∘w-1