po2ne

Description: Two sets related by a partial order are not equal. (Contributed by AV, 13-Mar-2023)

		Ref	Expression
	Assertion	po2ne	$⊢ (R Po V \land (A \in V \land B \in V) \land A R B) \to A \neq B$

Step	Hyp	Ref	Expression
1		breq1	$⊢ A = B \to (A R B \leftrightarrow B R B)$
2		poirr	$⊢ (R Po V \land B \in V) \to \neg B R B$
3	2	adantrl	$⊢ (R Po V \land (A \in V \land B \in V)) \to \neg B R B$
4	3	pm2.21d	$⊢ (R Po V \land (A \in V \land B \in V)) \to (B R B \to A \neq B)$
5	4	ex	$⊢ R Po V \to ((A \in V \land B \in V) \to (B R B \to A \neq B))$
6	5	com13	$⊢ B R B \to ((A \in V \land B \in V) \to (R Po V \to A \neq B))$
7	1 6	biimtrdi	$⊢ A = B \to (A R B \to ((A \in V \land B \in V) \to (R Po V \to A \neq B)))$
8	7	com24	$⊢ A = B \to (R Po V \to ((A \in V \land B \in V) \to (A R B \to A \neq B)))$
9	8	3impd	$⊢ A = B \to ((R Po V \land (A \in V \land B \in V) \land A R B) \to A \neq B)$
10		ax-1	$⊢ A \neq B \to ((R Po V \land (A \in V \land B \in V) \land A R B) \to A \neq B)$
11	9 10	pm2.61ine	$⊢ (R Po V \land (A \in V \land B \in V) \land A R B) \to A \neq B$

Metamath Proof Explorer