poltletr

Description: Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015)

		Ref	Expression
	Assertion	poltletr	$⊢ (R Po X \land (A \in X \land B \in X \land C \in X)) \to ((A R B \land B (R \cup I) C) \to A R C)$

Step	Hyp	Ref	Expression
1		poleloe	$⊢ C \in X \to (B (R \cup I) C \leftrightarrow (B R C \lor B = C))$
2	1	3ad2ant3	$⊢ (A \in X \land B \in X \land C \in X) \to (B (R \cup I) C \leftrightarrow (B R C \lor B = C))$
3	2	adantl	$⊢ (R Po X \land (A \in X \land B \in X \land C \in X)) \to (B (R \cup I) C \leftrightarrow (B R C \lor B = C))$
4	3	anbi2d	$⊢ (R Po X \land (A \in X \land B \in X \land C \in X)) \to ((A R B \land B (R \cup I) C) \leftrightarrow (A R B \land (B R C \lor B = C)))$
5		potr	$⊢ (R Po X \land (A \in X \land B \in X \land C \in X)) \to ((A R B \land B R C) \to A R C)$
6	5	com12	$⊢ (A R B \land B R C) \to ((R Po X \land (A \in X \land B \in X \land C \in X)) \to A R C)$
7		breq2	$⊢ B = C \to (A R B \leftrightarrow A R C)$
8	7	biimpac	$⊢ (A R B \land B = C) \to A R C$
9	8	a1d	$⊢ (A R B \land B = C) \to ((R Po X \land (A \in X \land B \in X \land C \in X)) \to A R C)$
10	6 9	jaodan	$⊢ (A R B \land (B R C \lor B = C)) \to ((R Po X \land (A \in X \land B \in X \land C \in X)) \to A R C)$
11	10	com12	$⊢ (R Po X \land (A \in X \land B \in X \land C \in X)) \to ((A R B \land (B R C \lor B = C)) \to A R C)$
12	4 11	sylbid	$⊢ (R Po X \land (A \in X \land B \in X \land C \in X)) \to ((A R B \land B (R \cup I) C) \to A R C)$

Metamath Proof Explorer