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 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴𝐵𝐵𝐴 ) ) )

Proof

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