Metamath Proof Explorer

Theorem ordtri2or

Description: A trichotomy law for ordinal classes. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)

		Ref	Expression
	Assertion	ordtri2or	$⊢ (Ord A \land Ord B) \to (A \in B \lor B \subseteq A)$

Step	Hyp	Ref	Expression
1		ordtri1	$⊢ (Ord B \land Ord A) \to (B \subseteq A \leftrightarrow \neg A \in B)$
2	1	ancoms	$⊢ (Ord A \land Ord B) \to (B \subseteq A \leftrightarrow \neg A \in B)$
3	2	biimprd	$⊢ (Ord A \land Ord B) \to (\neg A \in B \to B \subseteq A)$
4	3	orrd	$⊢ (Ord A \land Ord B) \to (A \in B \lor B \subseteq A)$