Metamath Proof Explorer

Theorem 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 ∧ Ord ⁡ B → A = B ↔ A ⊆ B ∧ ¬ A ∈ B

Proof

Step Hyp Ref Expression
1 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
2 ordtri1 ⊢ Ord ⁡ B ∧ Ord ⁡ A → B ⊆ A ↔ ¬ A ∈ B
3 2 ancoms ⊢ Ord ⁡ A ∧ Ord ⁡ B → B ⊆ A ↔ ¬ A ∈ B
4 3 anbi2d ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ∧ B ⊆ A ↔ A ⊆ B ∧ ¬ A ∈ B
5 1 4 bitrid ⊢ Ord ⁡ A ∧ Ord ⁡ B → A = B ↔ A ⊆ B ∧ ¬ A ∈ B