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 e. B \/ B e. A ) ) )

Proof

Step Hyp Ref Expression
1 ordirr 
 |-  ( Ord B -> -. B e. B )
2 1 adantl 
 |-  ( ( Ord A /\ Ord B ) -> -. B e. B )
3 eleq2 
 |-  ( A = B -> ( B e. A <-> B e. B ) )
4 3 notbid 
 |-  ( A = B -> ( -. B e. A <-> -. B e. B ) )
5 2 4 syl5ibrcom 
 |-  ( ( Ord A /\ Ord B ) -> ( A = B -> -. B e. A ) )
6 5 pm4.71d 
 |-  ( ( Ord A /\ Ord B ) -> ( A = B <-> ( A = B /\ -. B e. A ) ) )
7 pm5.61 
 |-  ( ( ( A = B \/ B e. A ) /\ -. B e. A ) <-> ( A = B /\ -. B e. A ) )
8 pm4.52 
 |-  ( ( ( A = B \/ B e. A ) /\ -. B e. A ) <-> -. ( -. ( A = B \/ B e. A ) \/ B e. A ) )
9 7 8 bitr3i 
 |-  ( ( A = B /\ -. B e. A ) <-> -. ( -. ( A = B \/ B e. A ) \/ B e. A ) )
10 6 9 bitrdi 
 |-  ( ( Ord A /\ Ord B ) -> ( A = B <-> -. ( -. ( A = B \/ B e. A ) \/ B e. A ) ) )
11 ordtri2 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> -. ( A = B \/ B e. A ) ) )
12 11 orbi1d 
 |-  ( ( Ord A /\ Ord B ) -> ( ( A e. B \/ B e. A ) <-> ( -. ( A = B \/ B e. A ) \/ B e. A ) ) )
13 12 notbid 
 |-  ( ( Ord A /\ Ord B ) -> ( -. ( A e. B \/ B e. A ) <-> -. ( -. ( A = B \/ B e. A ) \/ B e. A ) ) )
14 10 13 bitr4d 
 |-  ( ( Ord A /\ Ord B ) -> ( A = B <-> -. ( A e. B \/ B e. A ) ) )