Theorem pmtrfcnv

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

	Ref	Expression
Hypotheses	pmtrrn.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
	pmtrrn.r	⊢ 𝑅 = ran 𝑇
Assertion	pmtrfcnv	⊢ ( 𝐹 ∈ 𝑅 → ◡ 𝐹 = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2		pmtrrn.r	⊢ 𝑅 = ran 𝑇
3		eqid	⊢ dom ( 𝐹 ∖ I ) = dom ( 𝐹 ∖ I )
4	1 2 3	pmtrfrn	⊢ ( 𝐹 ∈ 𝑅 → ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) ) )
5	4	simpld	⊢ ( 𝐹 ∈ 𝑅 → ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) )
6	1	pmtrf	⊢ ( ( 𝐷 ∈ V ∧ dom ( 𝐹 ∖ I ) ⊆ 𝐷 ∧ dom ( 𝐹 ∖ I ) ≈ 2o ) → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 )
7	5 6	syl	⊢ ( 𝐹 ∈ 𝑅 → ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 )
8	4	simprd	⊢ ( 𝐹 ∈ 𝑅 → 𝐹 = ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) )
9	8	feq1d	⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 : 𝐷 ⟶ 𝐷 ↔ ( 𝑇 ‘ dom ( 𝐹 ∖ I ) ) : 𝐷 ⟶ 𝐷 ) )
10	7 9	mpbird	⊢ ( 𝐹 ∈ 𝑅 → 𝐹 : 𝐷 ⟶ 𝐷 )
11	1 2	pmtrfinv	⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐷 ) )
12	10 10 11 11	2fcoidinvd	⊢ ( 𝐹 ∈ 𝑅 → ◡ 𝐹 = 𝐹 )