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 \in V \land (X \in D \land Y \in D \land X \neq Y)) \to T (\{X, Y\}) (Y) = X$

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 \in D \land Y \in D) \leftrightarrow (Y \in D \land X \in D)$
6		necom	$⊢ X \neq Y \leftrightarrow Y \neq X$
7	5 6	anbi12i	$⊢ ((X \in D \land Y \in D) \land X \neq Y) \leftrightarrow ((Y \in D \land X \in D) \land Y \neq X)$
8		df-3an	$⊢ (X \in D \land Y \in D \land X \neq Y) \leftrightarrow ((X \in D \land Y \in D) \land X \neq Y)$
9		df-3an	$⊢ (Y \in D \land X \in D \land Y \neq X) \leftrightarrow ((Y \in D \land X \in D) \land Y \neq X)$
10	7 8 9	3bitr4i	$⊢ (X \in D \land Y \in D \land X \neq Y) \leftrightarrow (Y \in D \land X \in D \land Y \neq X)$
11	1	pmtrprfv	$⊢ (D \in V \land (Y \in D \land X \in D \land Y \neq X)) \to T (\{Y, X\}) (Y) = X$
12	10 11	sylan2b	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to T (\{Y, X\}) (Y) = X$
13	4 12	eqtr3id	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to T (\{X, Y\}) (Y) = X$

Metamath Proof Explorer