Metamath Proof Explorer

Theorem ordtri1

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

Ref Expression
Assertion ordtri1 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ∈ A

Proof

Step Hyp Ref Expression
1 ordsseleq ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ B ∨ A = B
2 ordn2lp ⊢ Ord ⁡ A → ¬ A ∈ B ∧ B ∈ A
3 imnan ⊢ A ∈ B → ¬ B ∈ A ↔ ¬ A ∈ B ∧ B ∈ A
4 2 3 sylibr ⊢ Ord ⁡ A → A ∈ B → ¬ B ∈ A
5 ordirr ⊢ Ord ⁡ B → ¬ B ∈ B
6 eleq2 ⊢ A = B → B ∈ A ↔ B ∈ B
7 6 notbid ⊢ A = B → ¬ B ∈ A ↔ ¬ B ∈ B
8 5 7 syl5ibrcom ⊢ Ord ⁡ B → A = B → ¬ B ∈ A
9 4 8 jaao ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ A = B → ¬ B ∈ A
10 ordtri3or ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ A = B ∨ B ∈ A
11 df-3or ⊢ A ∈ B ∨ A = B ∨ B ∈ A ↔ A ∈ B ∨ A = B ∨ B ∈ A
12 10 11 sylib ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ A = B ∨ B ∈ A
13 12 orcomd ⊢ Ord ⁡ A ∧ Ord ⁡ B → B ∈ A ∨ A ∈ B ∨ A = B
14 13 ord ⊢ Ord ⁡ A ∧ Ord ⁡ B → ¬ B ∈ A → A ∈ B ∨ A = B
15 9 14 impbid ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ A = B ↔ ¬ B ∈ A
16 1 15 bitrd ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ∈ A