Metamath Proof Explorer

Theorem issoi

Description: An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996) (Revised by Mario Carneiro, 9-Jul-2014)

		Ref	Expression
	Hypotheses	issoi.1	$⊢ x \in A \to \neg x R x$
		issoi.2	$⊢ (x \in A \land y \in A \land z \in A) \to ((x R y \land y R z) \to x R z)$
		issoi.3	$⊢ (x \in A \land y \in A) \to (x R y \lor x = y \lor y R x)$
	Assertion	issoi	$⊢ R Or A$

Proof

Step	Hyp	Ref	Expression
1		issoi.1	$⊢ x \in A \to \neg x R x$
2		issoi.2	$⊢ (x \in A \land y \in A \land z \in A) \to ((x R y \land y R z) \to x R z)$
3		issoi.3	$⊢ (x \in A \land y \in A) \to (x R y \lor x = y \lor y R x)$
4	1	adantl	$⊢ (⊤ \land x \in A) \to \neg x R x$
5	2	adantl	$⊢ (⊤ \land (x \in A \land y \in A \land z \in A)) \to ((x R y \land y R z) \to x R z)$
6	4 5	ispod	$⊢ ⊤ \to R Po A$
7	3	adantl	$⊢ (⊤ \land (x \in A \land y \in A)) \to (x R y \lor x = y \lor y R x)$
8	6 7	issod	$⊢ ⊤ \to R Or A$
9	8	mptru	$⊢ R Or A$