Theorem pmtrfcnv

Description: A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015)

	Ref	Expression
Hypotheses	pmtrrn.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
	pmtrrn.r	$$⊢R=\mathrm{ran}T$$
Assertion	pmtrfcnv	$$⊢F\in R\to F^{-1}=F$$

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
2		pmtrrn.r	$$⊢R=\mathrm{ran}T$$
3		eqid	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)=\mathrm{dom}\left(F\setminus \mathrm{I}\right)$$
4	1 2 3	pmtrfrn	$$⊢F\in R\to \left(\left(D\in \mathrm{V}\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)\wedge F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\right)$$
5	4	simpld	$$⊢F\in R\to \left(D\in \mathrm{V}\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)$$
6	1	pmtrf	$$⊢\left(D\in \mathrm{V}\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq D\wedge \mathrm{dom}\left(F\setminus \mathrm{I}\right)\approx 2_{𝑜}\right)\to T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right):D⟶D$$
7	5 6	syl	$$⊢F\in R\to T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right):D⟶D$$
8	4	simprd	$$⊢F\in R\to F=T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)$$
9	8	feq1d	$$⊢F\in R\to \left(F:D⟶D\leftrightarrow T\left(\mathrm{dom}\left(F\setminus \mathrm{I}\right)\right):D⟶D\right)$$
10	7 9	mpbird	$$⊢F\in R\to F:D⟶D$$
11	1 2	pmtrfinv	$$⊢F\in R\to F\circ F={\mathrm{I}\upharpoonright }_D$$
12	10 10 11 11	2fcoidinvd	$$⊢F\in R\to F^{-1}=F$$