This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordtri3or

Description: A trichotomy law for ordinals. Proposition 7.10 of TakeutiZaring p. 38. Theorem 1.9(iii) of Schloeder p. 1. (Contributed by NM, 10-May-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ordtri3or 
|- ( ( Ord A /\ Ord B ) -> ( A e. B \/ A = B \/ B e. A ) )

Proof

Step Hyp Ref Expression
1 ordin 
 |-  ( ( Ord A /\ Ord B ) -> Ord ( A i^i B ) )
2 ordirr 
 |-  ( Ord ( A i^i B ) -> -. ( A i^i B ) e. ( A i^i B ) )
3 1 2 syl 
 |-  ( ( Ord A /\ Ord B ) -> -. ( A i^i B ) e. ( A i^i B ) )
4 ianor 
 |-  ( -. ( ( A i^i B ) e. A /\ ( B i^i A ) e. B ) <-> ( -. ( A i^i B ) e. A \/ -. ( B i^i A ) e. B ) )
5 elin 
 |-  ( ( A i^i B ) e. ( A i^i B ) <-> ( ( A i^i B ) e. A /\ ( A i^i B ) e. B ) )
6 incom 
 |-  ( A i^i B ) = ( B i^i A )
7 6 eleq1i 
 |-  ( ( A i^i B ) e. B <-> ( B i^i A ) e. B )
8 7 anbi2i 
 |-  ( ( ( A i^i B ) e. A /\ ( A i^i B ) e. B ) <-> ( ( A i^i B ) e. A /\ ( B i^i A ) e. B ) )
9 5 8 bitri 
 |-  ( ( A i^i B ) e. ( A i^i B ) <-> ( ( A i^i B ) e. A /\ ( B i^i A ) e. B ) )
10 4 9 xchnxbir 
 |-  ( -. ( A i^i B ) e. ( A i^i B ) <-> ( -. ( A i^i B ) e. A \/ -. ( B i^i A ) e. B ) )
11 3 10 sylib 
 |-  ( ( Ord A /\ Ord B ) -> ( -. ( A i^i B ) e. A \/ -. ( B i^i A ) e. B ) )
12 inss1 
 |-  ( A i^i B ) C_ A
13 ordsseleq 
 |-  ( ( Ord ( A i^i B ) /\ Ord A ) -> ( ( A i^i B ) C_ A <-> ( ( A i^i B ) e. A \/ ( A i^i B ) = A ) ) )
14 12 13 mpbii 
 |-  ( ( Ord ( A i^i B ) /\ Ord A ) -> ( ( A i^i B ) e. A \/ ( A i^i B ) = A ) )
15 1 14 sylan 
 |-  ( ( ( Ord A /\ Ord B ) /\ Ord A ) -> ( ( A i^i B ) e. A \/ ( A i^i B ) = A ) )
16 15 anabss1 
 |-  ( ( Ord A /\ Ord B ) -> ( ( A i^i B ) e. A \/ ( A i^i B ) = A ) )
17 16 ord 
 |-  ( ( Ord A /\ Ord B ) -> ( -. ( A i^i B ) e. A -> ( A i^i B ) = A ) )
18 dfss2 
 |-  ( A C_ B <-> ( A i^i B ) = A )
19 17 18 imbitrrdi 
 |-  ( ( Ord A /\ Ord B ) -> ( -. ( A i^i B ) e. A -> A C_ B ) )
20 ordin 
 |-  ( ( Ord B /\ Ord A ) -> Ord ( B i^i A ) )
21 inss1 
 |-  ( B i^i A ) C_ B
22 ordsseleq 
 |-  ( ( Ord ( B i^i A ) /\ Ord B ) -> ( ( B i^i A ) C_ B <-> ( ( B i^i A ) e. B \/ ( B i^i A ) = B ) ) )
23 21 22 mpbii 
 |-  ( ( Ord ( B i^i A ) /\ Ord B ) -> ( ( B i^i A ) e. B \/ ( B i^i A ) = B ) )
24 20 23 sylan 
 |-  ( ( ( Ord B /\ Ord A ) /\ Ord B ) -> ( ( B i^i A ) e. B \/ ( B i^i A ) = B ) )
25 24 anabss4 
 |-  ( ( Ord A /\ Ord B ) -> ( ( B i^i A ) e. B \/ ( B i^i A ) = B ) )
26 25 ord 
 |-  ( ( Ord A /\ Ord B ) -> ( -. ( B i^i A ) e. B -> ( B i^i A ) = B ) )
27 dfss2 
 |-  ( B C_ A <-> ( B i^i A ) = B )
28 26 27 imbitrrdi 
 |-  ( ( Ord A /\ Ord B ) -> ( -. ( B i^i A ) e. B -> B C_ A ) )
29 19 28 orim12d 
 |-  ( ( Ord A /\ Ord B ) -> ( ( -. ( A i^i B ) e. A \/ -. ( B i^i A ) e. B ) -> ( A C_ B \/ B C_ A ) ) )
30 11 29 mpd 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )
31 sspsstri 
 |-  ( ( A C_ B \/ B C_ A ) <-> ( A C. B \/ A = B \/ B C. A ) )
32 30 31 sylib 
 |-  ( ( Ord A /\ Ord B ) -> ( A C. B \/ A = B \/ B C. A ) )
33 ordelpss 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B <-> A C. B ) )
34 biidd 
 |-  ( ( Ord A /\ Ord B ) -> ( A = B <-> A = B ) )
35 ordelpss 
 |-  ( ( Ord B /\ Ord A ) -> ( B e. A <-> B C. A ) )
36 35 ancoms 
 |-  ( ( Ord A /\ Ord B ) -> ( B e. A <-> B C. A ) )
37 33 34 36 3orbi123d 
 |-  ( ( Ord A /\ Ord B ) -> ( ( A e. B \/ A = B \/ B e. A ) <-> ( A C. B \/ A = B \/ B C. A ) ) )
38 32 37 mpbird 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B \/ A = B \/ B e. A ) )