Theorem pmtrdifel

Description: A transposition of elements of a set without a special element corresponds to a transposition of elements of the set. (Contributed by AV, 15-Jan-2019)

	Ref	Expression
Hypotheses	pmtrdifel.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)$$
	pmtrdifel.r	$$⊢R=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
Assertion	pmtrdifel	$$⊢\forall t\in T\exists r\in R\forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=r\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)$$
2		pmtrdifel.r	$$⊢R=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
3		eqid	$$⊢\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)$$
4	1 2 3	pmtrdifellem1	$$⊢t\in T\to \mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\in R$$
5	1 2 3	pmtrdifellem3	$$⊢t\in T\to \forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\left(x\right)$$
6		fveq1	$$⊢r=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\to r\left(x\right)=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\left(x\right)$$
7	6	eqeq2d	$$⊢r=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\to \left(t\left(x\right)=r\left(x\right)\leftrightarrow t\left(x\right)=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\left(x\right)\right)$$
8	7	ralbidv	$$⊢r=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\to \left(\forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=r\left(x\right)\leftrightarrow \forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\left(x\right)\right)$$
9	8	rspcev	$$⊢\left(\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\in R\wedge \forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(t\setminus \mathrm{I}\right)\right)\left(x\right)\right)\to \exists r\in R\forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=r\left(x\right)$$
10	4 5 9	syl2anc	$$⊢t\in T\to \exists r\in R\forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=r\left(x\right)$$
11	10	rgen	$$⊢\forall t\in T\exists r\in R\forall x\in \left(N\setminus \left\{K\right\}\right)t\left(x\right)=r\left(x\right)$$