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 ⊢Ord⁡A∧Ord⁡B→A⊆B↔¬B∈A

Proof

Step Hyp Ref Expression
1 ordsseleq ⊢Ord⁡A∧Ord⁡B→A⊆B↔A∈B∨A=B
2 ordn2lp ⊢Ord⁡A→¬A∈B∧B∈A
3 imnan ⊢A∈B→¬B∈A↔¬A∈B∧B∈A
4 2 3 sylibr ⊢Ord⁡A→A∈B→¬B∈A
5 ordirr ⊢Ord⁡B→¬B∈B
6 eleq2 ⊢A=B→B∈A↔B∈B
7 6 notbid ⊢A=B→¬B∈A↔¬B∈B
8 5 7 syl5ibrcom ⊢Ord⁡B→A=B→¬B∈A
9 4 8 jaao ⊢Ord⁡A∧Ord⁡B→A∈B∨A=B→¬B∈A
10 ordtri3or ⊢Ord⁡A∧Ord⁡B→A∈B∨A=B∨B∈A
11 df-3or ⊢A∈B∨A=B∨B∈A↔A∈B∨A=B∨B∈A
12 10 11 sylib ⊢Ord⁡A∧Ord⁡B→A∈B∨A=B∨B∈A
13 12 orcomd ⊢Ord⁡A∧Ord⁡B→B∈A∨A∈B∨A=B
14 13 ord ⊢Ord⁡A∧Ord⁡B→¬B∈A→A∈B∨A=B
15 9 14 impbid ⊢Ord⁡A∧Ord⁡B→A∈B∨A=B↔¬B∈A
16 1 15 bitrd ⊢Ord⁡A∧Ord⁡B→A⊆B↔¬B∈A