Theorem cyc2fvx

Description: Function value of a 2-cycle outside of its orbit. (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	cyc2fvx	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(K\right)=K$$

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	4 5	s2cld	$$⊢\phi \to ⟨“IJ”⟩\in \mathrm{Word}D$$
11	4 5 7	s2f1	$$⊢\phi \to ⟨“IJ”⟩:\mathrm{dom}⟨“IJ”⟩\underset{1-1}{⟶}D$$
12	8	necomd	$$⊢\phi \to K\ne J$$
13	9 12	nelprd	$$⊢\phi \to \neg K\in \left\{I,J\right\}$$
14	4 5	s2rn	$$⊢\phi \to \mathrm{ran}⟨“IJ”⟩=\left\{I,J\right\}$$
15	13 14	neleqtrrd	$$⊢\phi \to \neg K\in \mathrm{ran}⟨“IJ”⟩$$
16	1 3 10 11 6 15	cycpmfv3	$$⊢\phi \to C\left(⟨“IJ”⟩\right)\left(K\right)=K$$