# Metamath Proof Explorer

## Theorem ordtri2

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

Ref Expression
Assertion ordtri2 ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}\in {B}↔¬\left({A}={B}\vee {B}\in {A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ordsseleq ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{A}\right)\to \left({B}\subseteq {A}↔\left({B}\in {A}\vee {B}={A}\right)\right)$
2 eqcom ${⊢}{B}={A}↔{A}={B}$
3 2 orbi2i ${⊢}\left({B}\in {A}\vee {B}={A}\right)↔\left({B}\in {A}\vee {A}={B}\right)$
4 orcom ${⊢}\left({B}\in {A}\vee {A}={B}\right)↔\left({A}={B}\vee {B}\in {A}\right)$
5 3 4 bitri ${⊢}\left({B}\in {A}\vee {B}={A}\right)↔\left({A}={B}\vee {B}\in {A}\right)$
6 1 5 syl6bb ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{A}\right)\to \left({B}\subseteq {A}↔\left({A}={B}\vee {B}\in {A}\right)\right)$
7 ordtri1 ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{A}\right)\to \left({B}\subseteq {A}↔¬{A}\in {B}\right)$
8 6 7 bitr3d ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{A}\right)\to \left(\left({A}={B}\vee {B}\in {A}\right)↔¬{A}\in {B}\right)$
9 8 ancoms ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left(\left({A}={B}\vee {B}\in {A}\right)↔¬{A}\in {B}\right)$
10 9 con2bid ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}\in {B}↔¬\left({A}={B}\vee {B}\in {A}\right)\right)$