Theorem cycpm2cl

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

	Ref	Expression
Hypotheses	cycpm2.c	$$⊢C=\mathrm{toCyc}\left(D\right)$$
	cycpm2.d	$$⊢\phi \to D\in V$$
	cycpm2.i	$$⊢\phi \to I\in D$$
	cycpm2.j	$$⊢\phi \to J\in D$$
	cycpm2.1	$$⊢\phi \to I\ne J$$
	cycpm2cl.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
Assertion	cycpm2cl	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\in {\mathrm{Base}}_S$$

Proof

Step	Hyp	Ref	Expression
1		cycpm2.c	$$⊢C=\mathrm{toCyc}\left(D\right)$$
2		cycpm2.d	$$⊢\phi \to D\in V$$
3		cycpm2.i	$$⊢\phi \to I\in D$$
4		cycpm2.j	$$⊢\phi \to J\in D$$
5		cycpm2.1	$$⊢\phi \to I\ne J$$
6		cycpm2cl.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
7	3 4	s2cld	$$⊢\phi \to ⟨“IJ”⟩\in \mathrm{Word}D$$
8	3 4 5	s2f1	$$⊢\phi \to ⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D$$
9	1 2 7 8 6	cycpmcl	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\in {\mathrm{Base}}_S$$