Metamath Proof Explorer

Theorem ordtri2or2

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

Ref Expression
Assertion ordtri2or2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ∨ B ⊆ A

Proof

Step Hyp Ref Expression
1 ordtri2or ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ B ⊆ A
2 ordelss ⊢ Ord ⁡ B ∧ A ∈ B → A ⊆ B
3 2 ex ⊢ Ord ⁡ B → A ∈ B → A ⊆ B
4 3 orim1d ⊢ Ord ⁡ B → A ∈ B ∨ B ⊆ A → A ⊆ B ∨ B ⊆ A
5 4 adantl ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ B ⊆ A → A ⊆ B ∨ B ⊆ A
6 1 5 mpd ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ∨ B ⊆ A