Metamath Proof Explorer

Theorem hash2prd

Description: A set of size two is an unordered pair if it contains two different elements. (Contributed by Alexander van der Vekens, 9-Dec-2018) (Proof shortened by AV, 16-Jun-2022)

		Ref	Expression
	Assertion	hash2prd	$⊢ (P \in V \land \|P\| = 2) \to ((X \in P \land Y \in P \land X \neq Y) \to P = \{X, Y\})$

Proof

Step	Hyp	Ref	Expression
1		hash2prb	$⊢ P \in V \to (\|P\| = 2 \leftrightarrow \exists x \in P \exists y \in P (x \neq y \land P = \{x, y\}))$
2		simpr	$⊢ ((((x \in P \land y \in P) \land x \neq y) \land (X \in P \land Y \in P \land X \neq Y)) \land P = \{x, y\}) \to P = \{x, y\}$
3		3simpa	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X \in P \land Y \in P)$
4	3	ad2antlr	$⊢ ((((x \in P \land y \in P) \land x \neq y) \land (X \in P \land Y \in P \land X \neq Y)) \land P = \{x, y\}) \to (X \in P \land Y \in P)$
5		eleq2	$⊢ P = \{x, y\} \to (X \in P \leftrightarrow X \in \{x, y\})$
6		eleq2	$⊢ P = \{x, y\} \to (Y \in P \leftrightarrow Y \in \{x, y\})$
7	5 6	anbi12d	$⊢ P = \{x, y\} \to ((X \in P \land Y \in P) \leftrightarrow (X \in \{x, y\} \land Y \in \{x, y\}))$
8	7	adantl	$⊢ ((((x \in P \land y \in P) \land x \neq y) \land (X \in P \land Y \in P \land X \neq Y)) \land P = \{x, y\}) \to ((X \in P \land Y \in P) \leftrightarrow (X \in \{x, y\} \land Y \in \{x, y\}))$
9	4 8	mpbid	$⊢ ((((x \in P \land y \in P) \land x \neq y) \land (X \in P \land Y \in P \land X \neq Y)) \land P = \{x, y\}) \to (X \in \{x, y\} \land Y \in \{x, y\})$
10		prel12g	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (\{X, Y\} = \{x, y\} \leftrightarrow (X \in \{x, y\} \land Y \in \{x, y\}))$
11	10	ad2antlr	$⊢ ((((x \in P \land y \in P) \land x \neq y) \land (X \in P \land Y \in P \land X \neq Y)) \land P = \{x, y\}) \to (\{X, Y\} = \{x, y\} \leftrightarrow (X \in \{x, y\} \land Y \in \{x, y\}))$
12	9 11	mpbird	$⊢ ((((x \in P \land y \in P) \land x \neq y) \land (X \in P \land Y \in P \land X \neq Y)) \land P = \{x, y\}) \to \{X, Y\} = \{x, y\}$
13	2 12	eqtr4d	$⊢ ((((x \in P \land y \in P) \land x \neq y) \land (X \in P \land Y \in P \land X \neq Y)) \land P = \{x, y\}) \to P = \{X, Y\}$
14	13	exp31	$⊢ ((x \in P \land y \in P) \land x \neq y) \to ((X \in P \land Y \in P \land X \neq Y) \to (P = \{x, y\} \to P = \{X, Y\}))$
15	14	com23	$⊢ ((x \in P \land y \in P) \land x \neq y) \to (P = \{x, y\} \to ((X \in P \land Y \in P \land X \neq Y) \to P = \{X, Y\}))$
16	15	expimpd	$⊢ (x \in P \land y \in P) \to ((x \neq y \land P = \{x, y\}) \to ((X \in P \land Y \in P \land X \neq Y) \to P = \{X, Y\}))$
17	16	rexlimivv	$⊢ \exists x \in P \exists y \in P (x \neq y \land P = \{x, y\}) \to ((X \in P \land Y \in P \land X \neq Y) \to P = \{X, Y\})$
18	1 17	syl6bi	$⊢ P \in V \to (\|P\| = 2 \to ((X \in P \land Y \in P \land X \neq Y) \to P = \{X, Y\}))$
19	18	imp	$⊢ (P \in V \land \|P\| = 2) \to ((X \in P \land Y \in P \land X \neq Y) \to P = \{X, Y\})$