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=\mathrm{toCyc}\left(D\right)$$
	cycpm3.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
	cycpm3.d	$$⊢\phi \to D\in V$$
	cycpm3.i	$$⊢\phi \to I\in D$$
	cycpm3.j	$$⊢\phi \to J\in D$$
	cycpm3.k	$$⊢\phi \to K\in D$$
	cycpm3.1	$$⊢\phi \to I\ne J$$
	cycpm3.2	$$⊢\phi \to J\ne K$$
	cycpm3.3	$$⊢\phi \to K\ne I$$
Assertion	cycpm3cl2	$$⊢\phi \to C\left(⟨“IJK”⟩\right)\in C\left[{\left|.\right|}^{-1}\left[\left\{3\right\}\right]\right]$$

Proof

Step	Hyp	Ref	Expression
1		cycpm3.c	$$⊢C=\mathrm{toCyc}\left(D\right)$$
2		cycpm3.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
3		cycpm3.d	$$⊢\phi \to D\in V$$
4		cycpm3.i	$$⊢\phi \to I\in D$$
5		cycpm3.j	$$⊢\phi \to J\in D$$
6		cycpm3.k	$$⊢\phi \to K\in D$$
7		cycpm3.1	$$⊢\phi \to I\ne J$$
8		cycpm3.2	$$⊢\phi \to J\ne K$$
9		cycpm3.3	$$⊢\phi \to K\ne I$$
10		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
11	1 2 10	tocycf	$$⊢D\in V\to C:\left\{w\in \mathrm{Word}D|w:\mathrm{dom}w\underset{1-1}{⟶}D\right\}⟶{\mathrm{Base}}_S$$
12	3 11	syl	$$⊢\phi \to C:\left\{w\in \mathrm{Word}D|w:\mathrm{dom}w\underset{1-1}{⟶}D\right\}⟶{\mathrm{Base}}_S$$
13	12	ffnd	$$⊢\phi \to CFn\left\{w\in \mathrm{Word}D|w:\mathrm{dom}w\underset{1-1}{⟶}D\right\}$$
14		id	$$⊢w=⟨“IJK”⟩\to w=⟨“IJK”⟩$$
15		dmeq	$$⊢w=⟨“IJK”⟩\to \mathrm{dom}w=\mathrm{dom}⟨“IJK”⟩$$
16		eqidd	$$⊢w=⟨“IJK”⟩\to D=D$$
17	14 15 16	f1eq123d	$$⊢w=⟨“IJK”⟩\to \left(w:\mathrm{dom}w\underset{1-1}{⟶}D\leftrightarrow ⟨“IJK”⟩:\mathrm{dom}⟨“IJK”⟩\underset{1-1}{⟶}D\right)$$
18	4 5 6	s3cld	$$⊢\phi \to ⟨“IJK”⟩\in \mathrm{Word}D$$
19	4 5 6 7 8 9	s3f1	$$⊢\phi \to ⟨“IJK”⟩:\mathrm{dom}⟨“IJK”⟩\underset{1-1}{⟶}D$$
20	17 18 19	elrabd	$$⊢\phi \to ⟨“IJK”⟩\in \left\{w\in \mathrm{Word}D|w:\mathrm{dom}w\underset{1-1}{⟶}D\right\}$$
21		s3clhash	$$⊢⟨“IJK”⟩\in {\left|.\right|}^{-1}\left[\left\{3\right\}\right]$$
22	21	a1i	$$⊢\phi \to ⟨“IJK”⟩\in {\left|.\right|}^{-1}\left[\left\{3\right\}\right]$$
23	13 20 22	fnfvimad	$$⊢\phi \to C\left(⟨“IJK”⟩\right)\in C\left[{\left|.\right|}^{-1}\left[\left\{3\right\}\right]\right]$$