Theorem domtriord

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

	Ref	Expression
Assertion	domtriord	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\preccurlyeq B\leftrightarrow \neg B\prec A\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbth	$$⊢\left(B\preccurlyeq A\wedge A\preccurlyeq B\right)\to B\approx A$$
2	1	expcom	$$⊢A\preccurlyeq B\to \left(B\preccurlyeq A\to B\approx A\right)$$
3	2	a1i	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\preccurlyeq B\to \left(B\preccurlyeq A\to B\approx A\right)\right)$$
4		iman	$$⊢\left(B\preccurlyeq A\to B\approx A\right)\leftrightarrow \neg \left(B\preccurlyeq A\wedge \neg B\approx A\right)$$
5		brsdom	$$⊢B\prec A\leftrightarrow \left(B\preccurlyeq A\wedge \neg B\approx A\right)$$
6	4 5	xchbinxr	$$⊢\left(B\preccurlyeq A\to B\approx A\right)\leftrightarrow \neg B\prec A$$
7	3 6	imbitrdi	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\preccurlyeq B\to \neg B\prec A\right)$$
8		onelss	$$⊢B\in \mathrm{On}\to \left(A\in B\to A\subseteq B\right)$$
9		ssdomg	$$⊢B\in \mathrm{On}\to \left(A\subseteq B\to A\preccurlyeq B\right)$$
10	8 9	syld	$$⊢B\in \mathrm{On}\to \left(A\in B\to A\preccurlyeq B\right)$$
11	10	adantl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\in B\to A\preccurlyeq B\right)$$
12	11	con3d	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\neg A\preccurlyeq B\to \neg A\in B\right)$$
13		ontri1	$$⊢\left(B\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(B\subseteq A\leftrightarrow \neg A\in B\right)$$
14	13	ancoms	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(B\subseteq A\leftrightarrow \neg A\in B\right)$$
15	12 14	sylibrd	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\neg A\preccurlyeq B\to B\subseteq A\right)$$
16		ssdomg	$$⊢A\in \mathrm{On}\to \left(B\subseteq A\to B\preccurlyeq A\right)$$
17	16	adantr	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(B\subseteq A\to B\preccurlyeq A\right)$$
18	15 17	syld	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\neg A\preccurlyeq B\to B\preccurlyeq A\right)$$
19		ensym	$$⊢B\approx A\to A\approx B$$
20		endom	$$⊢A\approx B\to A\preccurlyeq B$$
21	19 20	syl	$$⊢B\approx A\to A\preccurlyeq B$$
22	21	con3i	$$⊢\neg A\preccurlyeq B\to \neg B\approx A$$
23	18 22	jca2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\neg A\preccurlyeq B\to \left(B\preccurlyeq A\wedge \neg B\approx A\right)\right)$$
24	23 5	syl6ibr	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\neg A\preccurlyeq B\to B\prec A\right)$$
25	24	con1d	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(\neg B\prec A\to A\preccurlyeq B\right)$$
26	7 25	impbid	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\preccurlyeq B\leftrightarrow \neg B\prec A\right)$$