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	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
	cycpm3.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
	cycpm3.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	cycpm3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
	cycpm3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
	cycpm3.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
	cycpm3.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
	cycpm3.2	⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
	cycpm3.3	⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
Assertion	cycpm3cl2	⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∈ ( 𝐶 “ ( ◡ ♯ “ { 3 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		cycpm3.c	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2		cycpm3.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3		cycpm3.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		cycpm3.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
5		cycpm3.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
6		cycpm3.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
7		cycpm3.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
8		cycpm3.2	⊢ ( 𝜑 → 𝐽 ≠ 𝐾 )
9		cycpm3.3	⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
10		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
11	1 2 10	tocycf	⊢ ( 𝐷 ∈ 𝑉 → 𝐶 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
12	3 11	syl	⊢ ( 𝜑 → 𝐶 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
13	12	ffnd	⊢ ( 𝜑 → 𝐶 Fn { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
14		id	⊢ ( 𝑤 = ⟨“ 𝐼 𝐽 𝐾 ”⟩ → 𝑤 = ⟨“ 𝐼 𝐽 𝐾 ”⟩ )
15		dmeq	⊢ ( 𝑤 = ⟨“ 𝐼 𝐽 𝐾 ”⟩ → dom 𝑤 = dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ )
16		eqidd	⊢ ( 𝑤 = ⟨“ 𝐼 𝐽 𝐾 ”⟩ → 𝐷 = 𝐷 )
17	14 15 16	f1eq123d	⊢ ( 𝑤 = ⟨“ 𝐼 𝐽 𝐾 ”⟩ → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ –1-1→ 𝐷 ) )
18	4 5 6	s3cld	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 )
19	4 5 6 7 8 9	s3f1	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ : dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ –1-1→ 𝐷 )
20	17 18 19	elrabd	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
21		s3clhash	⊢ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ ( ◡ ♯ “ { 3 } )
22	21	a1i	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ ( ◡ ♯ “ { 3 } ) )
23	13 20 22	fnfvimad	⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ∈ ( 𝐶 “ ( ◡ ♯ “ { 3 } ) ) )