3elpr2eq

Description: If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021)

		Ref	Expression
	Assertion	3elpr2eq	$⊢ ((X \in \{A, B\} \land Y \in \{A, B\} \land Z \in \{A, B\}) \land (Y \neq X \land Z \neq X)) \to Y = Z$

Proof

Step	Hyp	Ref	Expression
1		elpri	$⊢ X \in \{A, B\} \to (X = A \lor X = B)$
2		elpri	$⊢ Y \in \{A, B\} \to (Y = A \lor Y = B)$
3		elpri	$⊢ Z \in \{A, B\} \to (Z = A \lor Z = B)$
4		eqtr3	$⊢ (Z = A \land X = A) \to Z = X$
5		eqneqall	$⊢ Z = X \to (Z \neq X \to Y = Z)$
6	4 5	syl	$⊢ (Z = A \land X = A) \to (Z \neq X \to Y = Z)$
7	6	adantld	$⊢ (Z = A \land X = A) \to ((Y \neq X \land Z \neq X) \to Y = Z)$
8	7	ex	$⊢ Z = A \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z))$
9	8	a1d	$⊢ Z = A \to ((Y = A \lor Y = B) \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
10		eqtr3	$⊢ (Y = A \land X = A) \to Y = X$
11		eqneqall	$⊢ Y = X \to (Y \neq X \to (Z \neq X \to Y = Z))$
12	10 11	syl	$⊢ (Y = A \land X = A) \to (Y \neq X \to (Z \neq X \to Y = Z))$
13	12	impd	$⊢ (Y = A \land X = A) \to ((Y \neq X \land Z \neq X) \to Y = Z)$
14	13	ex	$⊢ Y = A \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z))$
15	14	a1d	$⊢ Y = A \to (Z = B \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
16		eqtr3	$⊢ (Y = B \land Z = B) \to Y = Z$
17	16	2a1d	$⊢ (Y = B \land Z = B) \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z))$
18	17	ex	$⊢ Y = B \to (Z = B \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
19	15 18	jaoi	$⊢ (Y = A \lor Y = B) \to (Z = B \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
20	19	com12	$⊢ Z = B \to ((Y = A \lor Y = B) \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
21	9 20	jaoi	$⊢ (Z = A \lor Z = B) \to ((Y = A \lor Y = B) \to (X = A \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
22	21	com13	$⊢ X = A \to ((Y = A \lor Y = B) \to ((Z = A \lor Z = B) \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
23		eqtr3	$⊢ (Y = A \land Z = A) \to Y = Z$
24	23	2a1d	$⊢ (Y = A \land Z = A) \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z))$
25	24	ex	$⊢ Y = A \to (Z = A \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
26		eqtr3	$⊢ (Y = B \land X = B) \to Y = X$
27	26 11	syl	$⊢ (Y = B \land X = B) \to (Y \neq X \to (Z \neq X \to Y = Z))$
28	27	impd	$⊢ (Y = B \land X = B) \to ((Y \neq X \land Z \neq X) \to Y = Z)$
29	28	ex	$⊢ Y = B \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z))$
30	29	a1d	$⊢ Y = B \to (Z = A \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
31	25 30	jaoi	$⊢ (Y = A \lor Y = B) \to (Z = A \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
32	31	com12	$⊢ Z = A \to ((Y = A \lor Y = B) \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
33		eqtr3	$⊢ (Z = B \land X = B) \to Z = X$
34	33 5	syl	$⊢ (Z = B \land X = B) \to (Z \neq X \to Y = Z)$
35	34	adantld	$⊢ (Z = B \land X = B) \to ((Y \neq X \land Z \neq X) \to Y = Z)$
36	35	ex	$⊢ Z = B \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z))$
37	36	a1d	$⊢ Z = B \to ((Y = A \lor Y = B) \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
38	32 37	jaoi	$⊢ (Z = A \lor Z = B) \to ((Y = A \lor Y = B) \to (X = B \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
39	38	com13	$⊢ X = B \to ((Y = A \lor Y = B) \to ((Z = A \lor Z = B) \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
40	22 39	jaoi	$⊢ (X = A \lor X = B) \to ((Y = A \lor Y = B) \to ((Z = A \lor Z = B) \to ((Y \neq X \land Z \neq X) \to Y = Z)))$
41	40	3imp	$⊢ ((X = A \lor X = B) \land (Y = A \lor Y = B) \land (Z = A \lor Z = B)) \to ((Y \neq X \land Z \neq X) \to Y = Z)$
42	1 2 3 41	syl3an	$⊢ (X \in \{A, B\} \land Y \in \{A, B\} \land Z \in \{A, B\}) \to ((Y \neq X \land Z \neq X) \to Y = Z)$
43	42	imp	$⊢ ((X \in \{A, B\} \land Y \in \{A, B\} \land Z \in \{A, B\}) \land (Y \neq X \land Z \neq X)) \to Y = Z$

Metamath Proof Explorer

Theorem 3elpr2eq

Proof