po2nr

Description: A partial order has no 2-cycle loops. (Contributed by NM, 27-Mar-1997)

		Ref	Expression
	Assertion	po2nr	$⊢ (R Po A \land (B \in A \land C \in A)) \to \neg (B R C \land C R B)$

Step	Hyp	Ref	Expression
1		poirr	$⊢ (R Po A \land B \in A) \to \neg B R B$
2	1	adantrr	$⊢ (R Po A \land (B \in A \land C \in A)) \to \neg B R B$
3		potr	$⊢ (R Po A \land (B \in A \land C \in A \land B \in A)) \to ((B R C \land C R B) \to B R B)$
4	3	3exp2	$⊢ R Po A \to (B \in A \to (C \in A \to (B \in A \to ((B R C \land C R B) \to B R B))))$
5	4	com34	$⊢ R Po A \to (B \in A \to (B \in A \to (C \in A \to ((B R C \land C R B) \to B R B))))$
6	5	pm2.43d	$⊢ R Po A \to (B \in A \to (C \in A \to ((B R C \land C R B) \to B R B)))$
7	6	imp32	$⊢ (R Po A \land (B \in A \land C \in A)) \to ((B R C \land C R B) \to B R B)$
8	2 7	mtod	$⊢ (R Po A \land (B \in A \land C \in A)) \to \neg (B R C \land C R B)$

Metamath Proof Explorer