Theorem ordtri3or 6298

Description: A trichotomy law for ordinals. Proposition 7.10 of [TakeutiZaring] p. 38. (Contributed by NM, 10-May-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
ordtri3or	⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))

Proof of Theorem ordtri3or

Step	Hyp	Ref	Expression
1		ordin 6296	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵))
2		ordirr 6284	. . . . . 6 ⊢ (Ord (𝐴 ∩ 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))
3	1, 2	syl 17	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))
4		ianor 979	. . . . . 6 ⊢ (¬ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵))
5		elin 3903	. . . . . . 7 ⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵))
6		incom 4135	. . . . . . . . 9 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
7	6	eleq1i 2829	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝐵 ↔ (𝐵 ∩ 𝐴) ∈ 𝐵)
8	7	anbi2i 623	. . . . . . 7 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵))
9	5, 8	bitri 274	. . . . . 6 ⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵))
10	4, 9	xchnxbir 333	. . . . 5 ⊢ (¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵))
11	3, 10	sylib 217	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵))
12		inss1 4162	. . . . . . . . . 10 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
13		ordsseleq 6295	. . . . . . . . . 10 ⊢ ((Ord (𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)))
14	12, 13	mpbii 232	. . . . . . . . 9 ⊢ ((Ord (𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))
15	1, 14	sylan 580	. . . . . . . 8 ⊢ (((Ord 𝐴 ∧ Ord 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))
16	15	anabss1 663	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))
17	16	ord 861	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → (𝐴 ∩ 𝐵) = 𝐴))
18		df-ss 3904	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
19	17, 18	syl6ibr 251	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → 𝐴 ⊆ 𝐵))
20		ordin 6296	. . . . . . . . 9 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → Ord (𝐵 ∩ 𝐴))
21		inss1 4162	. . . . . . . . . 10 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
22		ordsseleq 6295	. . . . . . . . . 10 ⊢ ((Ord (𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ⊆ 𝐵 ↔ ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)))
23	21, 22	mpbii 232	. . . . . . . . 9 ⊢ ((Ord (𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))
24	20, 23	sylan 580	. . . . . . . 8 ⊢ (((Ord 𝐵 ∧ Ord 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))
25	24	anabss4 664	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))
26	25	ord 861	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → (𝐵 ∩ 𝐴) = 𝐵))
27		df-ss 3904	. . . . . 6 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐵)
28	26, 27	syl6ibr 251	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → 𝐵 ⊆ 𝐴))
29	19, 28	orim12d 962	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)))
30	11, 29	mpd 15	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
31		sspsstri 4037	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
32	30, 31	sylib 217	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
33		ordelpss 6294	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵))
34		biidd 261	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ 𝐴 = 𝐵))
35		ordelpss 6294	. . . 4 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴))
36	35	ancoms 459	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴))
37	33, 34, 36	3orbi123d 1434	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)))
38	32, 37	mpbird 256	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∨ w3o 1085   = wceq 1539   ∈ wcel 2106   ∩ cin 3886   ⊆ wss 3887   ⊊ wpss 3888  Ord word 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269

This theorem is referenced by:  ordtri1  6299  epweon  7625  epweonOLD  7626  ordeleqon  7632  smo11  8195  smoord  8196  omopth2  8415  ttrcltr  9474  r111  9533  tcrank  9642  domtriomlem  10198  axdc3lem2  10207  zorn2lem6  10257  grur1  10576  poseq  33802  soseq  33803  nosepon  33868