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 \land Ord B) \to (A \in B \lor A = B \lor B \in A)$

Proof

Step	Hyp	Ref	Expression
1		ordin	$⊢ (Ord A \land Ord B) \to Ord (A \cap B)$
2		ordirr	$⊢ Ord (A \cap B) \to \neg A \cap B \in (A \cap B)$
3	1 2	syl	$⊢ (Ord A \land Ord B) \to \neg A \cap B \in (A \cap B)$
4		ianor	$⊢ \neg (A \cap B \in A \land B \cap A \in B) \leftrightarrow (\neg A \cap B \in A \lor \neg B \cap A \in B)$
5		elin	$⊢ A \cap B \in (A \cap B) \leftrightarrow (A \cap B \in A \land A \cap B \in B)$
6		incom	$⊢ A \cap B = B \cap A$
7	6	eleq1i	$⊢ A \cap B \in B \leftrightarrow B \cap A \in B$
8	7	anbi2i	$⊢ (A \cap B \in A \land A \cap B \in B) \leftrightarrow (A \cap B \in A \land B \cap A \in B)$
9	5 8	bitri	$⊢ A \cap B \in (A \cap B) \leftrightarrow (A \cap B \in A \land B \cap A \in B)$
10	4 9	xchnxbir	$⊢ \neg A \cap B \in (A \cap B) \leftrightarrow (\neg A \cap B \in A \lor \neg B \cap A \in B)$
11	3 10	sylib	$⊢ (Ord A \land Ord B) \to (\neg A \cap B \in A \lor \neg B \cap A \in B)$
12		inss1	$⊢ A \cap B \subseteq A$
13		ordsseleq	$⊢ (Ord (A \cap B) \land Ord A) \to (A \cap B \subseteq A \leftrightarrow (A \cap B \in A \lor A \cap B = A))$
14	12 13	mpbii	$⊢ (Ord (A \cap B) \land Ord A) \to (A \cap B \in A \lor A \cap B = A)$
15	1 14	sylan	$⊢ ((Ord A \land Ord B) \land Ord A) \to (A \cap B \in A \lor A \cap B = A)$
16	15	anabss1	$⊢ (Ord A \land Ord B) \to (A \cap B \in A \lor A \cap B = A)$
17	16	ord	$⊢ (Ord A \land Ord B) \to (\neg A \cap B \in A \to A \cap B = A)$
18		dfss2	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
19	17 18	imbitrrdi	$⊢ (Ord A \land Ord B) \to (\neg A \cap B \in A \to A \subseteq B)$
20		ordin	$⊢ (Ord B \land Ord A) \to Ord (B \cap A)$
21		inss1	$⊢ B \cap A \subseteq B$
22		ordsseleq	$⊢ (Ord (B \cap A) \land Ord B) \to (B \cap A \subseteq B \leftrightarrow (B \cap A \in B \lor B \cap A = B))$
23	21 22	mpbii	$⊢ (Ord (B \cap A) \land Ord B) \to (B \cap A \in B \lor B \cap A = B)$
24	20 23	sylan	$⊢ ((Ord B \land Ord A) \land Ord B) \to (B \cap A \in B \lor B \cap A = B)$
25	24	anabss4	$⊢ (Ord A \land Ord B) \to (B \cap A \in B \lor B \cap A = B)$
26	25	ord	$⊢ (Ord A \land Ord B) \to (\neg B \cap A \in B \to B \cap A = B)$
27		dfss2	$⊢ B \subseteq A \leftrightarrow B \cap A = B$
28	26 27	imbitrrdi	$⊢ (Ord A \land Ord B) \to (\neg B \cap A \in B \to B \subseteq A)$
29	19 28	orim12d	$⊢ (Ord A \land Ord B) \to ((\neg A \cap B \in A \lor \neg B \cap A \in B) \to (A \subseteq B \lor B \subseteq A))$
30	11 29	mpd	$⊢ (Ord A \land Ord B) \to (A \subseteq B \lor B \subseteq A)$
31		sspsstri	$⊢ (A \subseteq B \lor B \subseteq A) \leftrightarrow (A \subset B \lor A = B \lor B \subset A)$
32	30 31	sylib	$⊢ (Ord A \land Ord B) \to (A \subset B \lor A = B \lor B \subset A)$
33		ordelpss	$⊢ (Ord A \land Ord B) \to (A \in B \leftrightarrow A \subset B)$
34		biidd	$⊢ (Ord A \land Ord B) \to (A = B \leftrightarrow A = B)$
35		ordelpss	$⊢ (Ord B \land Ord A) \to (B \in A \leftrightarrow B \subset A)$
36	35	ancoms	$⊢ (Ord A \land Ord B) \to (B \in A \leftrightarrow B \subset A)$
37	33 34 36	3orbi123d	$⊢ (Ord A \land Ord B) \to ((A \in B \lor A = B \lor B \in A) \leftrightarrow (A \subset B \lor A = B \lor B \subset A))$
38	32 37	mpbird	$⊢ (Ord A \land Ord B) \to (A \in B \lor A = B \lor B \in A)$

Metamath Proof Explorer

Theorem ordtri3or

Proof