ordtri2or2

Description: A trichotomy law for ordinal classes. (Contributed by NM, 2-Nov-2003)

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

Step	Hyp	Ref	Expression
1		ordtri2or	$⊢ (Ord A \land Ord B) \to (A \in B \lor B \subseteq A)$
2		ordelss	$⊢ (Ord B \land A \in B) \to A \subseteq B$
3	2	ex	$⊢ Ord B \to (A \in B \to A \subseteq B)$
4	3	orim1d	$⊢ Ord B \to ((A \in B \lor B \subseteq A) \to (A \subseteq B \lor B \subseteq A))$
5	4	adantl	$⊢ (Ord A \land Ord B) \to ((A \in B \lor B \subseteq A) \to (A \subseteq B \lor B \subseteq A))$
6	1 5	mpd	$⊢ (Ord A \land Ord B) \to (A \subseteq B \lor B \subseteq A)$

Metamath Proof Explorer