Theorem cyc2fvx

Description: Function value of a 2-cycle outside of its orbit. (Contributed by Thierry Arnoux, 19-Sep-2023)

	Ref	Expression
Hypotheses	cycpm3.c	|- C = ( toCyc ` D )
	cycpm3.s	|- S = ( SymGrp ` D )
	cycpm3.d	|- ( ph -> D e. V )
	cycpm3.i	|- ( ph -> I e. D )
	cycpm3.j	|- ( ph -> J e. D )
	cycpm3.k	|- ( ph -> K e. D )
	cycpm3.1	|- ( ph -> I =/= J )
	cycpm3.2	|- ( ph -> J =/= K )
	cycpm3.3	|- ( ph -> K =/= I )
Assertion	cyc2fvx	|- ( ph -> ( ( C ` <" I J "> ) ` K ) = K )

Proof

Step	Hyp	Ref	Expression
1		cycpm3.c	|- C = ( toCyc ` D )
2		cycpm3.s	|- S = ( SymGrp ` D )
3		cycpm3.d	|- ( ph -> D e. V )
4		cycpm3.i	|- ( ph -> I e. D )
5		cycpm3.j	|- ( ph -> J e. D )
6		cycpm3.k	|- ( ph -> K e. D )
7		cycpm3.1	|- ( ph -> I =/= J )
8		cycpm3.2	|- ( ph -> J =/= K )
9		cycpm3.3	|- ( ph -> K =/= I )
10	4 5	s2cld	|- ( ph -> <" I J "> e. Word D )
11	4 5 7	s2f1	|- ( ph -> <" I J "> : dom <" I J "> -1-1-> D )
12	8	necomd	|- ( ph -> K =/= J )
13	9 12	nelprd	|- ( ph -> -. K e. { I , J } )
14	4 5	s2rn	|- ( ph -> ran <" I J "> = { I , J } )
15	13 14	neleqtrrd	|- ( ph -> -. K e. ran <" I J "> )
16	1 3 10 11 6 15	cycpmfv3	|- ( ph -> ( ( C ` <" I J "> ) ` K ) = K )