Theorem ordtri3or 6398

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

Assertion

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

Proof of Theorem ordtri3or

Step	Hyp	Ref	Expression
1		ordin 6396	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵))
2		ordirr 6383	. . . . . 6 ⊢ (Ord (𝐴 ∩ 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))
3	1, 2	syl 18	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))
4		ianor 997	. . . . . 6 ⊢ (¬ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵))
5		elin 4092	. . . . . . 7 ⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵))
6		incom 4105	. . . . . . . . 9 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
7	6	eleq1i 2851	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐵) ∈ 𝐵 ↔ (𝐵 ∩ 𝐴) ∈ 𝐵)
8	7	anbi2i 635	. . . . . . 7 ⊢ (((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵))
9	5, 8	bitri 278	. . . . . 6 ⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵))
10	4, 9	xchnxbir 336	. . . . 5 ⊢ (¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵))
11	3, 10	sylib 221	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵))
12		inss1 4132	. . . . . . . . . 10 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
13		ordsseleq 6395	. . . . . . . . . 10 ⊢ ((Ord (𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)))
14	12, 13	mpbii 236	. . . . . . . . 9 ⊢ ((Ord (𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))
15	1, 14	sylan 592	. . . . . . . 8 ⊢ (((Ord 𝐴 ∧ Ord 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))
16	15	anabss1 679	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))
17	16	ord 878	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → (𝐴 ∩ 𝐵) = 𝐴))
18		dfss2 4093	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴)
19	17, 18	imbitrrdi 255	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → 𝐴 ⊆ 𝐵))
20		ordin 6396	. . . . . . . . 9 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → Ord (𝐵 ∩ 𝐴))
21		inss1 4132	. . . . . . . . . 10 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵
22		ordsseleq 6395	. . . . . . . . . 10 ⊢ ((Ord (𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ⊆ 𝐵 ↔ ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)))
23	21, 22	mpbii 236	. . . . . . . . 9 ⊢ ((Ord (𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))
24	20, 23	sylan 592	. . . . . . . 8 ⊢ (((Ord 𝐵 ∧ Ord 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))
25	24	anabss4 680	. . . . . . 7 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))
26	25	ord 878	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → (𝐵 ∩ 𝐴) = 𝐵))
27		dfss2 4093	. . . . . 6 ⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐵)
28	26, 27	imbitrrdi 255	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → 𝐵 ⊆ 𝐴))
29	19, 28	orim12d 979	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)))
30	11, 29	mpd 16	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
31		sspsstri 4032	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
32	30, 31	sylib 221	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))
33		ordelpss 6393	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵))
34		biidd 265	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ 𝐴 = 𝐵))
35		ordelpss 6393	. . . 4 ⊢ ((Ord 𝐵 ∧ Ord 𝐴) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴))
36	35	ancoms 464	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴))
37	33, 34, 36	3orbi123d 1463	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)))
38	32, 37	mpbird 260	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   = wceq 1569   ∈ wcel 2144   ⊆ wss 3896   ⊊ wpss 4012   ∩ cin 4088  Ord word 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368

This theorem is used by:  ordtri1  6399  oneltri  6409  epweon  7793  epweonALT  7794  ordeleqon  7800  poseq  8181  soseq  8182  smo11  8379  smoord  8380  omopth2  8599  ttrcltr  9724  r111  9789  tcrank  9908  domtriomlem  10527  axdc3lem2  10536  zorn2lem6  10586  grur1  10912  nosepon  28031  addsproplem7  28370  negsproplem7  28429  mulsproplem13  28523  mulsproplem14  28524