Theorem cycpm3cl2

Description: Closure of the 3-cycles in the class of 3-cycles. (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	cycpm3cl2	|- ( ph -> ( C ` <" I J K "> ) e. ( C " ( `' # " { 3 } ) ) )

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		eqid	|- ( Base ` S ) = ( Base ` S )
11	1 2 10	tocycf	|- ( D e. V -> C : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
12	3 11	syl	|- ( ph -> C : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) )
13	12	ffnd	|- ( ph -> C Fn { w e. Word D | w : dom w -1-1-> D } )
14		id	|- ( w = <" I J K "> -> w = <" I J K "> )
15		dmeq	|- ( w = <" I J K "> -> dom w = dom <" I J K "> )
16		eqidd	|- ( w = <" I J K "> -> D = D )
17	14 15 16	f1eq123d	|- ( w = <" I J K "> -> ( w : dom w -1-1-> D <-> <" I J K "> : dom <" I J K "> -1-1-> D ) )
18	4 5 6	s3cld	|- ( ph -> <" I J K "> e. Word D )
19	4 5 6 7 8 9	s3f1	|- ( ph -> <" I J K "> : dom <" I J K "> -1-1-> D )
20	17 18 19	elrabd	|- ( ph -> <" I J K "> e. { w e. Word D | w : dom w -1-1-> D } )
21		s3clhash	|- <" I J K "> e. ( `' # " { 3 } )
22	21	a1i	|- ( ph -> <" I J K "> e. ( `' # " { 3 } ) )
23	13 20 22	fnfvimad	|- ( ph -> ( C ` <" I J K "> ) e. ( C " ( `' # " { 3 } ) ) )