Theorem cycpm2tr

Description: A cyclic permutation of 2 elements is a transposition. (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$$
	cycpm2tr.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
Assertion	cycpm2tr	$$⊢\phi \to C\left(⟨“IJ”⟩\right)=T\left(\left\{I,J\right\}\right)$$

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		cycpm2tr.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
7		partfun	$$⊢\left(x\in D⟼if\left(x\in \left\{I,J\right\},\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right),x\right)\right)=\left(x\in \left(D\cap \left\{I,J\right\}\right)⟼\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)\right)\cup \left(x\in \left(D\setminus \left\{I,J\right\}\right)⟼x\right)$$
8	7	a1i	$$⊢\phi \to \left(x\in D⟼if\left(x\in \left\{I,J\right\},\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right),x\right)\right)=\left(x\in \left(D\cap \left\{I,J\right\}\right)⟼\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)\right)\cup \left(x\in \left(D\setminus \left\{I,J\right\}\right)⟼x\right)$$
9		cshw1s2	$$⊢\left(I\in D\wedge J\in D\right)\to ⟨“IJ”⟩\mathrm{cyclShift}1=⟨“JI”⟩$$
10	3 4 9	syl2anc	$$⊢\phi \to ⟨“IJ”⟩\mathrm{cyclShift}1=⟨“JI”⟩$$
11	10	coeq1d	$$⊢\phi \to \left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}=⟨“JI”⟩\circ {⟨“IJ”⟩}^{-1}$$
12		0nn0	$$⊢0\in {\mathbb{N}}_0$$
13	12	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
14		1nn0	$$⊢1\in {\mathbb{N}}_0$$
15	14	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
16		0ne1	$$⊢0\ne 1$$
17	16	a1i	$$⊢\phi \to 0\ne 1$$
18	13 4 15 3 17 3 4 5	coprprop	$$⊢\phi \to \left\{⟨0,J⟩,⟨1,I⟩\right\}\circ \left\{⟨I,0⟩,⟨J,1⟩\right\}=\left\{⟨I,J⟩,⟨J,I⟩\right\}$$
19		s2prop	$$⊢\left(J\in D\wedge I\in D\right)\to ⟨“JI”⟩=\left\{⟨0,J⟩,⟨1,I⟩\right\}$$
20	4 3 19	syl2anc	$$⊢\phi \to ⟨“JI”⟩=\left\{⟨0,J⟩,⟨1,I⟩\right\}$$
21		s2prop	$$⊢\left(I\in D\wedge J\in D\right)\to ⟨“IJ”⟩=\left\{⟨0,I⟩,⟨1,J⟩\right\}$$
22	3 4 21	syl2anc	$$⊢\phi \to ⟨“IJ”⟩=\left\{⟨0,I⟩,⟨1,J⟩\right\}$$
23	22	cnveqd	$$⊢\phi \to {⟨“IJ”⟩}^{-1}={\left\{⟨0,I⟩,⟨1,J⟩\right\}}^{-1}$$
24		cnvprop	$$⊢\left(\left(0\in {\mathbb{N}}_0\wedge I\in D\right)\wedge \left(1\in {\mathbb{N}}_0\wedge J\in D\right)\right)\to {\left\{⟨0,I⟩,⟨1,J⟩\right\}}^{-1}=\left\{⟨I,0⟩,⟨J,1⟩\right\}$$
25	13 3 15 4 24	syl22anc	$$⊢\phi \to {\left\{⟨0,I⟩,⟨1,J⟩\right\}}^{-1}=\left\{⟨I,0⟩,⟨J,1⟩\right\}$$
26	23 25	eqtrd	$$⊢\phi \to {⟨“IJ”⟩}^{-1}=\left\{⟨I,0⟩,⟨J,1⟩\right\}$$
27	20 26	coeq12d	$$⊢\phi \to ⟨“JI”⟩\circ {⟨“IJ”⟩}^{-1}=\left\{⟨0,J⟩,⟨1,I⟩\right\}\circ \left\{⟨I,0⟩,⟨J,1⟩\right\}$$
28	3 4 4 3 5	mptprop	$$⊢\phi \to \left\{⟨I,J⟩,⟨J,I⟩\right\}=\left(x\in \left\{I,J\right\}⟼if\left(x=I,J,I\right)\right)$$
29		incom	$$⊢\left\{I,J\right\}\cap D=D\cap \left\{I,J\right\}$$
30	3 4	prssd	$$⊢\phi \to \left\{I,J\right\}\subseteq D$$
31		df-ss	$$⊢\left\{I,J\right\}\subseteq D\leftrightarrow \left\{I,J\right\}\cap D=\left\{I,J\right\}$$
32	30 31	sylib	$$⊢\phi \to \left\{I,J\right\}\cap D=\left\{I,J\right\}$$
33	29 32	syl5reqr	$$⊢\phi \to \left\{I,J\right\}=D\cap \left\{I,J\right\}$$
34		simpr	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge x=I\right)\to x=I$$
35	34	sneqd	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge x=I\right)\to \left\{x\right\}=\left\{I\right\}$$
36	35	difeq2d	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge x=I\right)\to \left\{I,J\right\}\setminus \left\{x\right\}=\left\{I,J\right\}\setminus \left\{I\right\}$$
37	36	unieqd	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge x=I\right)\to \bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)=\bigcup \left(\left\{I,J\right\}\setminus \left\{I\right\}\right)$$
38		difprsn1	$$⊢I\ne J\to \left\{I,J\right\}\setminus \left\{I\right\}=\left\{J\right\}$$
39	38	unieqd	$$⊢I\ne J\to \bigcup \left(\left\{I,J\right\}\setminus \left\{I\right\}\right)=\bigcup \left\{J\right\}$$
40	5 39	syl	$$⊢\phi \to \bigcup \left(\left\{I,J\right\}\setminus \left\{I\right\}\right)=\bigcup \left\{J\right\}$$
41		unisng	$$⊢J\in D\to \bigcup \left\{J\right\}=J$$
42	4 41	syl	$$⊢\phi \to \bigcup \left\{J\right\}=J$$
43	40 42	eqtrd	$$⊢\phi \to \bigcup \left(\left\{I,J\right\}\setminus \left\{I\right\}\right)=J$$
44	43	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge x=I\right)\to \bigcup \left(\left\{I,J\right\}\setminus \left\{I\right\}\right)=J$$
45	37 44	eqtr2d	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge x=I\right)\to J=\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)$$
46		vex	$$⊢x\in \mathrm{V}$$
47	46	elpr	$$⊢x\in \left\{I,J\right\}\leftrightarrow \left(x=I\vee x=J\right)$$
48		df-or	$$⊢\left(x=I\vee x=J\right)\leftrightarrow \left(\neg x=I\to x=J\right)$$
49	47 48	sylbb	$$⊢x\in \left\{I,J\right\}\to \left(\neg x=I\to x=J\right)$$
50	49	imp	$$⊢\left(x\in \left\{I,J\right\}\wedge \neg x=I\right)\to x=J$$
51	50	adantll	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge \neg x=I\right)\to x=J$$
52	51	sneqd	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge \neg x=I\right)\to \left\{x\right\}=\left\{J\right\}$$
53	52	difeq2d	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge \neg x=I\right)\to \left\{I,J\right\}\setminus \left\{x\right\}=\left\{I,J\right\}\setminus \left\{J\right\}$$
54	53	unieqd	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge \neg x=I\right)\to \bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)=\bigcup \left(\left\{I,J\right\}\setminus \left\{J\right\}\right)$$
55		difprsn2	$$⊢I\ne J\to \left\{I,J\right\}\setminus \left\{J\right\}=\left\{I\right\}$$
56	55	unieqd	$$⊢I\ne J\to \bigcup \left(\left\{I,J\right\}\setminus \left\{J\right\}\right)=\bigcup \left\{I\right\}$$
57	5 56	syl	$$⊢\phi \to \bigcup \left(\left\{I,J\right\}\setminus \left\{J\right\}\right)=\bigcup \left\{I\right\}$$
58		unisng	$$⊢I\in D\to \bigcup \left\{I\right\}=I$$
59	3 58	syl	$$⊢\phi \to \bigcup \left\{I\right\}=I$$
60	57 59	eqtrd	$$⊢\phi \to \bigcup \left(\left\{I,J\right\}\setminus \left\{J\right\}\right)=I$$
61	60	ad2antrr	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge \neg x=I\right)\to \bigcup \left(\left\{I,J\right\}\setminus \left\{J\right\}\right)=I$$
62	54 61	eqtr2d	$$⊢\left(\left(\phi \wedge x\in \left\{I,J\right\}\right)\wedge \neg x=I\right)\to I=\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)$$
63	45 62	ifeqda	$$⊢\left(\phi \wedge x\in \left\{I,J\right\}\right)\to if\left(x=I,J,I\right)=\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)$$
64	33 63	mpteq12dva	$$⊢\phi \to \left(x\in \left\{I,J\right\}⟼if\left(x=I,J,I\right)\right)=\left(x\in \left(D\cap \left\{I,J\right\}\right)⟼\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)\right)$$
65	28 64	eqtr2d	$$⊢\phi \to \left(x\in \left(D\cap \left\{I,J\right\}\right)⟼\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)\right)=\left\{⟨I,J⟩,⟨J,I⟩\right\}$$
66	18 27 65	3eqtr4d	$$⊢\phi \to ⟨“JI”⟩\circ {⟨“IJ”⟩}^{-1}=\left(x\in \left(D\cap \left\{I,J\right\}\right)⟼\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)\right)$$
67	11 66	eqtrd	$$⊢\phi \to \left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}=\left(x\in \left(D\cap \left\{I,J\right\}\right)⟼\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)\right)$$
68	3 4	s2rn	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩=\left\{I,J\right\}$$
69	68	difeq2d	$$⊢\phi \to D\setminus \mathrm{ran}⟨“IJ”⟩=D\setminus \left\{I,J\right\}$$
70	69	reseq2d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}={\mathrm{I}\upharpoonright }_{\left(D\setminus \left\{I,J\right\}\right)}$$
71		mptresid	$$⊢{\mathrm{I}\upharpoonright }_{\left(D\setminus \left\{I,J\right\}\right)}=\left(x\in \left(D\setminus \left\{I,J\right\}\right)⟼x\right)$$
72	70 71	eqtrdi	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}=\left(x\in \left(D\setminus \left\{I,J\right\}\right)⟼x\right)$$
73	67 72	uneq12d	$$⊢\phi \to \left(\left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}\right)\cup \left({\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}\right)=\left(x\in \left(D\cap \left\{I,J\right\}\right)⟼\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right)\right)\cup \left(x\in \left(D\setminus \left\{I,J\right\}\right)⟼x\right)$$
74		uncom	$$⊢\left(\left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}\right)\cup \left({\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}\right)=\left({\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}\right)\cup \left(\left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}\right)$$
75	74	a1i	$$⊢\phi \to \left(\left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}\right)\cup \left({\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}\right)=\left({\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}\right)\cup \left(\left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}\right)$$
76	8 73 75	3eqtr2rd	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}\right)\cup \left(\left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}\right)=\left(x\in D⟼if\left(x\in \left\{I,J\right\},\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right),x\right)\right)$$
77	3 4	s2cld	$$⊢\phi \to ⟨“IJ”⟩\in \mathrm{Word}D$$
78	3 4 5	s2f1	$$⊢\phi \to ⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D$$
79	1 2 77 78	tocycfv	$$⊢\phi \to C\left(⟨“IJ”⟩\right)=\left({\mathrm{I}\upharpoonright }_{\left(D\setminus \mathrm{ran}⟨“IJ”⟩\right)}\right)\cup \left(\left(⟨“IJ”⟩\mathrm{cyclShift}1\right)\circ {⟨“IJ”⟩}^{-1}\right)$$
80		pr2nelem	$$⊢\left(I\in D\wedge J\in D\wedge I\ne J\right)\to \left\{I,J\right\}\approx 2_{𝑜}$$
81	3 4 5 80	syl3anc	$$⊢\phi \to \left\{I,J\right\}\approx 2_{𝑜}$$
82	6	pmtrval	$$⊢\left(D\in V\wedge \left\{I,J\right\}\subseteq D\wedge \left\{I,J\right\}\approx 2_{𝑜}\right)\to T\left(\left\{I,J\right\}\right)=\left(x\in D⟼if\left(x\in \left\{I,J\right\},\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right),x\right)\right)$$
83	2 30 81 82	syl3anc	$$⊢\phi \to T\left(\left\{I,J\right\}\right)=\left(x\in D⟼if\left(x\in \left\{I,J\right\},\bigcup \left(\left\{I,J\right\}\setminus \left\{x\right\}\right),x\right)\right)$$
84	76 79 83	3eqtr4d	$$⊢\phi \to C\left(⟨“IJ”⟩\right)=T\left(\left\{I,J\right\}\right)$$