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

Proof

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