Theorem domtriord

Description: Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009)

	Ref	Expression
Assertion	domtriord	|- ( ( A e. On /\ B e. On ) -> ( A ~<_ B <-> -. B ~< A ) )

Proof

Step	Hyp	Ref	Expression
1		sbth	|- ( ( B ~<_ A /\ A ~<_ B ) -> B ~~ A )
2	1	expcom	|- ( A ~<_ B -> ( B ~<_ A -> B ~~ A ) )
3	2	a1i	|- ( ( A e. On /\ B e. On ) -> ( A ~<_ B -> ( B ~<_ A -> B ~~ A ) ) )
4		iman	|- ( ( B ~<_ A -> B ~~ A ) <-> -. ( B ~<_ A /\ -. B ~~ A ) )
5		brsdom	|- ( B ~< A <-> ( B ~<_ A /\ -. B ~~ A ) )
6	4 5	xchbinxr	|- ( ( B ~<_ A -> B ~~ A ) <-> -. B ~< A )
7	3 6	imbitrdi	|- ( ( A e. On /\ B e. On ) -> ( A ~<_ B -> -. B ~< A ) )
8		onelss	|- ( B e. On -> ( A e. B -> A C_ B ) )
9		ssdomg	|- ( B e. On -> ( A C_ B -> A ~<_ B ) )
10	8 9	syld	|- ( B e. On -> ( A e. B -> A ~<_ B ) )
11	10	adantl	|- ( ( A e. On /\ B e. On ) -> ( A e. B -> A ~<_ B ) )
12	11	con3d	|- ( ( A e. On /\ B e. On ) -> ( -. A ~<_ B -> -. A e. B ) )
13		ontri1	|- ( ( B e. On /\ A e. On ) -> ( B C_ A <-> -. A e. B ) )
14	13	ancoms	|- ( ( A e. On /\ B e. On ) -> ( B C_ A <-> -. A e. B ) )
15	12 14	sylibrd	|- ( ( A e. On /\ B e. On ) -> ( -. A ~<_ B -> B C_ A ) )
16		ssdomg	|- ( A e. On -> ( B C_ A -> B ~<_ A ) )
17	16	adantr	|- ( ( A e. On /\ B e. On ) -> ( B C_ A -> B ~<_ A ) )
18	15 17	syld	|- ( ( A e. On /\ B e. On ) -> ( -. A ~<_ B -> B ~<_ A ) )
19		ensym	|- ( B ~~ A -> A ~~ B )
20		endom	|- ( A ~~ B -> A ~<_ B )
21	19 20	syl	|- ( B ~~ A -> A ~<_ B )
22	21	con3i	|- ( -. A ~<_ B -> -. B ~~ A )
23	18 22	jca2	|- ( ( A e. On /\ B e. On ) -> ( -. A ~<_ B -> ( B ~<_ A /\ -. B ~~ A ) ) )
24	23 5	imbitrrdi	|- ( ( A e. On /\ B e. On ) -> ( -. A ~<_ B -> B ~< A ) )
25	24	con1d	|- ( ( A e. On /\ B e. On ) -> ( -. B ~< A -> A ~<_ B ) )
26	7 25	impbid	|- ( ( A e. On /\ B e. On ) -> ( A ~<_ B <-> -. B ~< A ) )