# 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 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}={B}↔¬\left({A}\in {B}\vee {B}\in {A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ordirr ${⊢}\mathrm{Ord}{B}\to ¬{B}\in {B}$
2 1 adantl ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to ¬{B}\in {B}$
3 eleq2 ${⊢}{A}={B}\to \left({B}\in {A}↔{B}\in {B}\right)$
4 3 notbid ${⊢}{A}={B}\to \left(¬{B}\in {A}↔¬{B}\in {B}\right)$
5 2 4 syl5ibrcom ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}={B}\to ¬{B}\in {A}\right)$
6 5 pm4.71d ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}={B}↔\left({A}={B}\wedge ¬{B}\in {A}\right)\right)$
7 pm5.61 ${⊢}\left(\left({A}={B}\vee {B}\in {A}\right)\wedge ¬{B}\in {A}\right)↔\left({A}={B}\wedge ¬{B}\in {A}\right)$
8 pm4.52 ${⊢}\left(\left({A}={B}\vee {B}\in {A}\right)\wedge ¬{B}\in {A}\right)↔¬\left(¬\left({A}={B}\vee {B}\in {A}\right)\vee {B}\in {A}\right)$
9 7 8 bitr3i ${⊢}\left({A}={B}\wedge ¬{B}\in {A}\right)↔¬\left(¬\left({A}={B}\vee {B}\in {A}\right)\vee {B}\in {A}\right)$
10 6 9 syl6bb ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}={B}↔¬\left(¬\left({A}={B}\vee {B}\in {A}\right)\vee {B}\in {A}\right)\right)$
11 ordtri2 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}\in {B}↔¬\left({A}={B}\vee {B}\in {A}\right)\right)$
12 11 orbi1d ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left(\left({A}\in {B}\vee {B}\in {A}\right)↔\left(¬\left({A}={B}\vee {B}\in {A}\right)\vee {B}\in {A}\right)\right)$
13 12 notbid ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left(¬\left({A}\in {B}\vee {B}\in {A}\right)↔¬\left(¬\left({A}={B}\vee {B}\in {A}\right)\vee {B}\in {A}\right)\right)$
14 10 13 bitr4d ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}={B}↔¬\left({A}\in {B}\vee {B}\in {A}\right)\right)$