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 ) )