ordtri4

Description: A trichotomy law for ordinals. (Contributed by NM, 1-Nov-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

		Ref	Expression
	Assertion	ordtri4	$⊢ (Ord A \land Ord B) \to (A = B \leftrightarrow (A \subseteq B \land \neg A \in B))$

Step	Hyp	Ref	Expression
1		eqss	$⊢ A = B \leftrightarrow (A \subseteq B \land B \subseteq A)$
2		ordtri1	$⊢ (Ord B \land Ord A) \to (B \subseteq A \leftrightarrow \neg A \in B)$
3	2	ancoms	$⊢ (Ord A \land Ord B) \to (B \subseteq A \leftrightarrow \neg A \in B)$
4	3	anbi2d	$⊢ (Ord A \land Ord B) \to ((A \subseteq B \land B \subseteq A) \leftrightarrow (A \subseteq B \land \neg A \in B))$
5	1 4	bitrid	$⊢ (Ord A \land Ord B) \to (A = B \leftrightarrow (A \subseteq B \land \neg A \in B))$

Metamath Proof Explorer