poprelb

Description: Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023)

		Ref	Expression
	Assertion	poprelb	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (\{A, B\} = \{C, D\} \leftrightarrow (A = C \land B = D))$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (A \in X \land B \in X)$
2		an3	$⊢ ((Rel R \land R Po X) \land (A R B \land C R D)) \to (Rel R \land C R D)$
3	2	3adant2	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (Rel R \land C R D)$
4		brrelex12	$⊢ (Rel R \land C R D) \to (C \in V \land D \in V)$
5	3 4	syl	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (C \in V \land D \in V)$
6		preq12bg	$⊢ ((A \in X \land B \in X) \land (C \in V \land D \in V)) \to (\{A, B\} = \{C, D\} \leftrightarrow ((A = C \land B = D) \lor (A = D \land B = C)))$
7	1 5 6	syl2anc	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (\{A, B\} = \{C, D\} \leftrightarrow ((A = C \land B = D) \lor (A = D \land B = C)))$
8		idd	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to ((A = C \land B = D) \to (A = C \land B = D))$
9		breq12	$⊢ (B = C \land A = D) \to (B R A \leftrightarrow C R D)$
10	9	ancoms	$⊢ (A = D \land B = C) \to (B R A \leftrightarrow C R D)$
11	10	bicomd	$⊢ (A = D \land B = C) \to (C R D \leftrightarrow B R A)$
12	11	anbi2d	$⊢ (A = D \land B = C) \to ((A R B \land C R D) \leftrightarrow (A R B \land B R A))$
13		po2nr	$⊢ (R Po X \land (A \in X \land B \in X)) \to \neg (A R B \land B R A)$
14	13	adantll	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X)) \to \neg (A R B \land B R A)$
15	14	pm2.21d	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X)) \to ((A R B \land B R A) \to (A = C \land B = D))$
16	15	ex	$⊢ (Rel R \land R Po X) \to ((A \in X \land B \in X) \to ((A R B \land B R A) \to (A = C \land B = D)))$
17	16	com13	$⊢ (A R B \land B R A) \to ((A \in X \land B \in X) \to ((Rel R \land R Po X) \to (A = C \land B = D)))$
18	12 17	biimtrdi	$⊢ (A = D \land B = C) \to ((A R B \land C R D) \to ((A \in X \land B \in X) \to ((Rel R \land R Po X) \to (A = C \land B = D))))$
19	18	com23	$⊢ (A = D \land B = C) \to ((A \in X \land B \in X) \to ((A R B \land C R D) \to ((Rel R \land R Po X) \to (A = C \land B = D))))$
20	19	com14	$⊢ (Rel R \land R Po X) \to ((A \in X \land B \in X) \to ((A R B \land C R D) \to ((A = D \land B = C) \to (A = C \land B = D))))$
21	20	3imp	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to ((A = D \land B = C) \to (A = C \land B = D))$
22	8 21	jaod	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (((A = C \land B = D) \lor (A = D \land B = C)) \to (A = C \land B = D))$
23		orc	$⊢ (A = C \land B = D) \to ((A = C \land B = D) \lor (A = D \land B = C))$
24	22 23	impbid1	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (((A = C \land B = D) \lor (A = D \land B = C)) \leftrightarrow (A = C \land B = D))$
25	7 24	bitrd	$⊢ ((Rel R \land R Po X) \land (A \in X \land B \in X) \land (A R B \land C R D)) \to (\{A, B\} = \{C, D\} \leftrightarrow (A = C \land B = D))$

Metamath Proof Explorer

Theorem poprelb

Proof