This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pmtrfcnv

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

Ref Expression
Hypotheses pmtrrn.t ⊢ T = pmTrsp ⁡ D
pmtrrn.r ⊢ R = ran ⁡ T
Assertion pmtrfcnv ⊢ F ∈ R → F -1 = F

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢ T = pmTrsp ⁡ D
2 pmtrrn.r ⊢ R = ran ⁡ T
3 eqid ⊢ dom ⁡ F ∖ I = dom ⁡ F ∖ I
4 1 2 3 pmtrfrn ⊢ F ∈ R → D ∈ V ∧ dom ⁡ F ∖ I ⊆ D ∧ dom ⁡ F ∖ I ≈ 2 𝑜 ∧ F = T ⁡ dom ⁡ F ∖ I
5 4 simpld ⊢ F ∈ R → D ∈ V ∧ dom ⁡ F ∖ I ⊆ D ∧ dom ⁡ F ∖ I ≈ 2 𝑜
6 1 pmtrf ⊢ D ∈ V ∧ dom ⁡ F ∖ I ⊆ D ∧ dom ⁡ F ∖ I ≈ 2 𝑜 → T ⁡ dom ⁡ F ∖ I : D ⟶ D
7 5 6 syl ⊢ F ∈ R → T ⁡ dom ⁡ F ∖ I : D ⟶ D
8 4 simprd ⊢ F ∈ R → F = T ⁡ dom ⁡ F ∖ I
9 8 feq1d ⊢ F ∈ R → F : D ⟶ D ↔ T ⁡ dom ⁡ F ∖ I : D ⟶ D
10 7 9 mpbird ⊢ F ∈ R → F : D ⟶ D
11 1 2 pmtrfinv ⊢ F ∈ R → F ∘ F = I ↾ D
12 10 10 11 11 2fcoidinvd ⊢ F ∈ R → F -1 = F