Metamath Proof Explorer

Theorem ordtri2

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Nov-1995)

Ref Expression
Assertion ordtri2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ ¬ A = B ∨ B ∈ A

Proof

Step Hyp Ref Expression
1 ordsseleq ⊢ Ord ⁡ B ∧ Ord ⁡ A → B ⊆ A ↔ B ∈ A ∨ B = A
2 eqcom ⊢ B = A ↔ A = B
3 2 orbi2i ⊢ B ∈ A ∨ B = A ↔ B ∈ A ∨ A = B
4 orcom ⊢ B ∈ A ∨ A = B ↔ A = B ∨ B ∈ A
5 3 4 bitri ⊢ B ∈ A ∨ B = A ↔ A = B ∨ B ∈ A
6 1 5 bitrdi ⊢ Ord ⁡ B ∧ Ord ⁡ A → B ⊆ A ↔ A = B ∨ B ∈ A
7 ordtri1 ⊢ Ord ⁡ B ∧ Ord ⁡ A → B ⊆ A ↔ ¬ A ∈ B
8 6 7 bitr3d ⊢ Ord ⁡ B ∧ Ord ⁡ A → A = B ∨ B ∈ A ↔ ¬ A ∈ B
9 8 ancoms ⊢ Ord ⁡ A ∧ Ord ⁡ B → A = B ∨ B ∈ A ↔ ¬ A ∈ B
10 9 con2bid ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ ¬ A = B ∨ B ∈ A