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

Metamath Proof Explorer

Theorem domtriord

Proof