sotr3

Description: Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021)

		Ref	Expression
	Assertion	sotr3	$⊢ (R Or A \land (X \in A \land Y \in A \land Z \in A)) \to ((X R Y \land \neg Z R Y) \to X R Z)$

Step	Hyp	Ref	Expression
1		simp3	$⊢ (X \in A \land Y \in A \land Z \in A) \to Z \in A$
2		simp2	$⊢ (X \in A \land Y \in A \land Z \in A) \to Y \in A$
3	1 2	jca	$⊢ (X \in A \land Y \in A \land Z \in A) \to (Z \in A \land Y \in A)$
4		sotric	$⊢ (R Or A \land (Z \in A \land Y \in A)) \to (Z R Y \leftrightarrow \neg (Z = Y \lor Y R Z))$
5	3 4	sylan2	$⊢ (R Or A \land (X \in A \land Y \in A \land Z \in A)) \to (Z R Y \leftrightarrow \neg (Z = Y \lor Y R Z))$
6	5	con2bid	$⊢ (R Or A \land (X \in A \land Y \in A \land Z \in A)) \to ((Z = Y \lor Y R Z) \leftrightarrow \neg Z R Y)$
7	6	adantr	$⊢ ((R Or A \land (X \in A \land Y \in A \land Z \in A)) \land X R Y) \to ((Z = Y \lor Y R Z) \leftrightarrow \neg Z R Y)$
8		breq2	$⊢ Z = Y \to (X R Z \leftrightarrow X R Y)$
9	8	biimprcd	$⊢ X R Y \to (Z = Y \to X R Z)$
10	9	adantl	$⊢ ((R Or A \land (X \in A \land Y \in A \land Z \in A)) \land X R Y) \to (Z = Y \to X R Z)$
11		sotr	$⊢ (R Or A \land (X \in A \land Y \in A \land Z \in A)) \to ((X R Y \land Y R Z) \to X R Z)$
12	11	expdimp	$⊢ ((R Or A \land (X \in A \land Y \in A \land Z \in A)) \land X R Y) \to (Y R Z \to X R Z)$
13	10 12	jaod	$⊢ ((R Or A \land (X \in A \land Y \in A \land Z \in A)) \land X R Y) \to ((Z = Y \lor Y R Z) \to X R Z)$
14	7 13	sylbird	$⊢ ((R Or A \land (X \in A \land Y \in A \land Z \in A)) \land X R Y) \to (\neg Z R Y \to X R Z)$
15	14	expimpd	$⊢ (R Or A \land (X \in A \land Y \in A \land Z \in A)) \to ((X R Y \land \neg Z R Y) \to X R Z)$

Metamath Proof Explorer