pmtrprfv3

Description: In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019)

		Ref	Expression
	Hypothesis	pmtrfval.t	$⊢ T = pmTrsp (D)$
	Assertion	pmtrprfv3	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to T (\{X, Y\}) (Z) = Z$

Proof

Step	Hyp	Ref	Expression
1		pmtrfval.t	$⊢ T = pmTrsp (D)$
2		simp1	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to D \in V$
3		simp1	$⊢ (X \in D \land Y \in D \land Z \in D) \to X \in D$
4	3	3ad2ant2	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to X \in D$
5		simp22	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Y \in D$
6	4 5	prssd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \{X, Y\} \subseteq D$
7		pr2nelem	$⊢ (X \in D \land Y \in D \land X \neq Y) \to \{X, Y\} \approx 2_{𝑜}$
8	7	3expia	$⊢ (X \in D \land Y \in D) \to (X \neq Y \to \{X, Y\} \approx 2_{𝑜})$
9	8	3adant3	$⊢ (X \in D \land Y \in D \land Z \in D) \to (X \neq Y \to \{X, Y\} \approx 2_{𝑜})$
10	9	com12	$⊢ X \neq Y \to ((X \in D \land Y \in D \land Z \in D) \to \{X, Y\} \approx 2_{𝑜})$
11	10	3ad2ant1	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to ((X \in D \land Y \in D \land Z \in D) \to \{X, Y\} \approx 2_{𝑜})$
12	11	impcom	$⊢ ((X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \{X, Y\} \approx 2_{𝑜}$
13	12	3adant1	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \{X, Y\} \approx 2_{𝑜}$
14		simp23	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Z \in D$
15	1	pmtrfv	$⊢ ((D \in V \land \{X, Y\} \subseteq D \land \{X, Y\} \approx 2_{𝑜}) \land Z \in D) \to T (\{X, Y\}) (Z) = if (Z \in \{X, Y\}, ⋃ (\{X, Y\} ∖ \{Z\}), Z)$
16	2 6 13 14 15	syl31anc	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to T (\{X, Y\}) (Z) = if (Z \in \{X, Y\}, ⋃ (\{X, Y\} ∖ \{Z\}), Z)$
17		necom	$⊢ X \neq Z \leftrightarrow Z \neq X$
18	17	biimpi	$⊢ X \neq Z \to Z \neq X$
19	18	3ad2ant2	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to Z \neq X$
20	19	3ad2ant3	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Z \neq X$
21		necom	$⊢ Y \neq Z \leftrightarrow Z \neq Y$
22	21	biimpi	$⊢ Y \neq Z \to Z \neq Y$
23	22	3ad2ant3	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to Z \neq Y$
24	23	3ad2ant3	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Z \neq Y$
25	20 24	nelprd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to \neg Z \in \{X, Y\}$
26	25	iffalsed	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to if (Z \in \{X, Y\}, ⋃ (\{X, Y\} ∖ \{Z\}), Z) = Z$
27	16 26	eqtrd	$⊢ (D \in V \land (X \in D \land Y \in D \land Z \in D) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to T (\{X, Y\}) (Z) = Z$

Metamath Proof Explorer

Theorem pmtrprfv3

Proof