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

### Proof

Step Hyp Ref Expression
1 ordsseleq ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}\subseteq {B}↔\left({A}\in {B}\vee {A}={B}\right)\right)$
2 ordn2lp ${⊢}\mathrm{Ord}{A}\to ¬\left({A}\in {B}\wedge {B}\in {A}\right)$
3 imnan ${⊢}\left({A}\in {B}\to ¬{B}\in {A}\right)↔¬\left({A}\in {B}\wedge {B}\in {A}\right)$
4 2 3 sylibr ${⊢}\mathrm{Ord}{A}\to \left({A}\in {B}\to ¬{B}\in {A}\right)$
5 ordirr ${⊢}\mathrm{Ord}{B}\to ¬{B}\in {B}$
6 eleq2 ${⊢}{A}={B}\to \left({B}\in {A}↔{B}\in {B}\right)$
7 6 notbid ${⊢}{A}={B}\to \left(¬{B}\in {A}↔¬{B}\in {B}\right)$
8 5 7 syl5ibrcom ${⊢}\mathrm{Ord}{B}\to \left({A}={B}\to ¬{B}\in {A}\right)$
9 4 8 jaao ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left(\left({A}\in {B}\vee {A}={B}\right)\to ¬{B}\in {A}\right)$
10 ordtri3or ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}\in {B}\vee {A}={B}\vee {B}\in {A}\right)$
11 df-3or ${⊢}\left({A}\in {B}\vee {A}={B}\vee {B}\in {A}\right)↔\left(\left({A}\in {B}\vee {A}={B}\right)\vee {B}\in {A}\right)$
12 10 11 sylib ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left(\left({A}\in {B}\vee {A}={B}\right)\vee {B}\in {A}\right)$
13 12 orcomd ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({B}\in {A}\vee \left({A}\in {B}\vee {A}={B}\right)\right)$
14 13 ord ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left(¬{B}\in {A}\to \left({A}\in {B}\vee {A}={B}\right)\right)$
15 9 14 impbid ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left(\left({A}\in {B}\vee {A}={B}\right)↔¬{B}\in {A}\right)$
16 1 15 bitrd ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}\subseteq {B}↔¬{B}\in {A}\right)$