This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordtri3

Description: A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by JJ, 24-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 ordirr ⊢ Ord ⁡ B → ¬ B ∈ B
2 1 adantl ⊢ Ord ⁡ A ∧ Ord ⁡ B → ¬ B ∈ B
3 eleq2 ⊢ A = B → B ∈ A ↔ B ∈ B
4 3 notbid ⊢ A = B → ¬ B ∈ A ↔ ¬ B ∈ B
5 2 4 syl5ibrcom ⊢ Ord ⁡ A ∧ Ord ⁡ B → A = B → ¬ B ∈ A
6 5 pm4.71d ⊢ Ord ⁡ A ∧ Ord ⁡ B → A = B ↔ A = B ∧ ¬ B ∈ A
7 pm5.61 ⊢ A = B ∨ B ∈ A ∧ ¬ B ∈ A ↔ A = B ∧ ¬ B ∈ A
8 pm4.52 ⊢ A = B ∨ B ∈ A ∧ ¬ B ∈ A ↔ ¬ ¬ A = B ∨ B ∈ A ∨ B ∈ A
9 7 8 bitr3i ⊢ A = B ∧ ¬ B ∈ A ↔ ¬ ¬ A = B ∨ B ∈ A ∨ B ∈ A
10 6 9 bitrdi ⊢ Ord ⁡ A ∧ Ord ⁡ B → A = B ↔ ¬ ¬ A = B ∨ B ∈ A ∨ B ∈ A
11 ordtri2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ ¬ A = B ∨ B ∈ A
12 11 orbi1d ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ B ∈ A ↔ ¬ A = B ∨ B ∈ A ∨ B ∈ A
13 12 notbid ⊢ Ord ⁡ A ∧ Ord ⁡ B → ¬ A ∈ B ∨ B ∈ A ↔ ¬ ¬ A = B ∨ B ∈ A ∨ B ∈ A
14 10 13 bitr4d ⊢ Ord ⁡ A ∧ Ord ⁡ B → A = B ↔ ¬ A ∈ B ∨ B ∈ A