Theorem cycpm2cl

Description: Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	cycpm2.c	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
	cycpm2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	cycpm2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
	cycpm2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
	cycpm2.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
	cycpm2cl.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
Assertion	cycpm2cl	⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		cycpm2.c	⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2		cycpm2.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		cycpm2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
4		cycpm2.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
5		cycpm2.1	⊢ ( 𝜑 → 𝐼 ≠ 𝐽 )
6		cycpm2cl.s	⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
7	3 4	s2cld	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
8	3 4 5	s2f1	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ : dom ⟨“ 𝐼 𝐽 ”⟩ –1-1→ 𝐷 )
9	1 2 7 8 6	cycpmcl	⊢ ( 𝜑 → ( 𝐶 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ∈ ( Base ‘ 𝑆 ) )