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 e. V -> C = ( w e. { u e. Word D | u : dom u -1-1-> D } |-> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tocycval.1	|- C = ( toCyc ` D )
2		df-tocyc	|- toCyc = ( d e. _V |-> ( w e. { u e. Word d | u : dom u -1-1-> d } |-> ( ( _I |` ( d \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )
3		wrdeq	|- ( d = D -> Word d = Word D )
4		f1eq3	|- ( d = D -> ( u : dom u -1-1-> d <-> u : dom u -1-1-> D ) )
5	3 4	rabeqbidv	|- ( d = D -> { u e. Word d | u : dom u -1-1-> d } = { u e. Word D | u : dom u -1-1-> D } )
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 ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) = ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) )
9	5 8	mpteq12dv	|- ( d = D -> ( w e. { u e. Word d | u : dom u -1-1-> d } |-> ( ( _I |` ( d \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) = ( w e. { u e. Word D | u : dom u -1-1-> D } |-> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )
10		elex	|- ( D e. V -> D e. _V )
11		eqid	|- { u e. Word D | u : dom u -1-1-> D } = { u e. Word D | u : dom u -1-1-> D }
12		wrdexg	|- ( D e. V -> Word D e. _V )
13	11 12	rabexd	|- ( D e. V -> { u e. Word D | u : dom u -1-1-> D } e. _V )
14	13	mptexd	|- ( D e. V -> ( w e. { u e. Word D | u : dom u -1-1-> D } |-> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) e. _V )
15	2 9 10 14	fvmptd3	|- ( D e. V -> ( toCyc ` D ) = ( w e. { u e. Word D | u : dom u -1-1-> D } |-> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )
16	1 15	syl5eq	|- ( D e. V -> C = ( w e. { u e. Word D | u : dom u -1-1-> D } |-> ( ( _I |` ( D \ ran w ) ) u. ( ( w cyclShift 1 ) o. `' w ) ) ) )