Metamath Proof Explorer

Theorem pmtrprfv2

Description: In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypothesis pmtrprfv2.t ⊢ T = pmTrsp ⁡ D
Assertion pmtrprfv2 ⊢ D ∈ V ∧ X ∈ D ∧ Y ∈ D ∧ X ≠ Y → T ⁡ X Y ⁡ Y = X

Proof

Step Hyp Ref Expression
1 pmtrprfv2.t ⊢ T = pmTrsp ⁡ D
2 prcom ⊢ Y X = X Y
3 2 fveq2i ⊢ T ⁡ Y X = T ⁡ X Y
4 3 fveq1i ⊢ T ⁡ Y X ⁡ Y = T ⁡ X Y ⁡ Y
5 ancom ⊢ X ∈ D ∧ Y ∈ D ↔ Y ∈ D ∧ X ∈ D
6 necom ⊢ X ≠ Y ↔ Y ≠ X
7 5 6 anbi12i ⊢ X ∈ D ∧ Y ∈ D ∧ X ≠ Y ↔ Y ∈ D ∧ X ∈ D ∧ Y ≠ X
8 df-3an ⊢ X ∈ D ∧ Y ∈ D ∧ X ≠ Y ↔ X ∈ D ∧ Y ∈ D ∧ X ≠ Y
9 df-3an ⊢ Y ∈ D ∧ X ∈ D ∧ Y ≠ X ↔ Y ∈ D ∧ X ∈ D ∧ Y ≠ X
10 7 8 9 3bitr4i ⊢ X ∈ D ∧ Y ∈ D ∧ X ≠ Y ↔ Y ∈ D ∧ X ∈ D ∧ Y ≠ X
11 1 pmtrprfv ⊢ D ∈ V ∧ Y ∈ D ∧ X ∈ D ∧ Y ≠ X → T ⁡ Y X ⁡ Y = X
12 10 11 sylan2b ⊢ D ∈ V ∧ X ∈ D ∧ Y ∈ D ∧ X ≠ Y → T ⁡ Y X ⁡ Y = X
13 4 12 eqtr3id ⊢ D ∈ V ∧ X ∈ D ∧ Y ∈ D ∧ X ≠ Y → T ⁡ X Y ⁡ Y = X