pmtrprfv

Description: In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		pmtrfval.t	$⊢ T = pmTrsp (D)$
2		simpl	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to D \in V$
3		simpr1	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to X \in D$
4		simpr2	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to Y \in D$
5	3 4	prssd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to \{X, Y\} \subseteq D$
6		enpr2	$⊢ (X \in D \land Y \in D \land X \neq Y) \to \{X, Y\} \approx 2_{𝑜}$
7	6	adantl	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to \{X, Y\} \approx 2_{𝑜}$
8	1	pmtrfv	$⊢ ((D \in V \land \{X, Y\} \subseteq D \land \{X, Y\} \approx 2_{𝑜}) \land X \in D) \to T (\{X, Y\}) (X) = if (X \in \{X, Y\}, ⋃ (\{X, Y\} ∖ \{X\}), X)$
9	2 5 7 3 8	syl31anc	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to T (\{X, Y\}) (X) = if (X \in \{X, Y\}, ⋃ (\{X, Y\} ∖ \{X\}), X)$
10		prid1g	$⊢ X \in D \to X \in \{X, Y\}$
11	3 10	syl	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to X \in \{X, Y\}$
12	11	iftrued	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to if (X \in \{X, Y\}, ⋃ (\{X, Y\} ∖ \{X\}), X) = ⋃ (\{X, Y\} ∖ \{X\})$
13		difprsnss	$⊢ \{X, Y\} ∖ \{X\} \subseteq \{Y\}$
14	13	a1i	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to \{X, Y\} ∖ \{X\} \subseteq \{Y\}$
15		prid2g	$⊢ Y \in D \to Y \in \{X, Y\}$
16	4 15	syl	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to Y \in \{X, Y\}$
17		simpr3	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to X \neq Y$
18	17	necomd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to Y \neq X$
19		eldifsn	$⊢ Y \in (\{X, Y\} ∖ \{X\}) \leftrightarrow (Y \in \{X, Y\} \land Y \neq X)$
20	16 18 19	sylanbrc	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to Y \in (\{X, Y\} ∖ \{X\})$
21	20	snssd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to \{Y\} \subseteq \{X, Y\} ∖ \{X\}$
22	14 21	eqssd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to \{X, Y\} ∖ \{X\} = \{Y\}$
23	22	unieqd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to ⋃ (\{X, Y\} ∖ \{X\}) = ⋃ \{Y\}$
24		unisng	$⊢ Y \in D \to ⋃ \{Y\} = Y$
25	4 24	syl	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to ⋃ \{Y\} = Y$
26	23 25	eqtrd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to ⋃ (\{X, Y\} ∖ \{X\}) = Y$
27	12 26	eqtrd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to if (X \in \{X, Y\}, ⋃ (\{X, Y\} ∖ \{X\}), X) = Y$
28	9 27	eqtrd	$⊢ (D \in V \land (X \in D \land Y \in D \land X \neq Y)) \to T (\{X, Y\}) (X) = Y$

Metamath Proof Explorer

Theorem pmtrprfv

Proof