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 ∧ Ord ⁡ B → A ∈ B ∨ B ⊆ A

Proof

Step Hyp Ref Expression
1 ordtri1 ⊢ Ord ⁡ B ∧ Ord ⁡ A → B ⊆ A ↔ ¬ A ∈ B
2 1 ancoms ⊢ Ord ⁡ A ∧ Ord ⁡ B → B ⊆ A ↔ ¬ A ∈ B
3 2 biimprd ⊢ Ord ⁡ A ∧ Ord ⁡ B → ¬ A ∈ B → B ⊆ A
4 3 orrd ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ B ⊆ A