Theorem ordtri1 6394

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
ordtri1	⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Proof of Theorem ordtri1

Step	Hyp	Ref	Expression
1		ordsseleq 6390	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
2		ordn2lp 6380	. . . . 5 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
3		imnan 404	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
4	2, 3	sylibr 237	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴))
5		ordirr 6378	. . . . 5 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
6		eleq2 2852	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵))
7	6	notbid 321	. . . . 5 ⊢ (𝐴 = 𝐵 → (¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵))
8	5, 7	syl5ibrcom 250	. . . 4 ⊢ (Ord 𝐵 → (𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴))
9	4, 8	jaao 969	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) → ¬ 𝐵 ∈ 𝐴))
10		ordtri3or 6393	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
11		df-3or 1104	. . . . . 6 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ∨ 𝐵 ∈ 𝐴))
12	10, 11	sylib 221	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ∨ 𝐵 ∈ 𝐴))
13	12	orcomd 884	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ∨ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
14	13	ord 877	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ 𝐵 ∈ 𝐴 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
15	9, 14	impbid 215	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ↔ ¬ 𝐵 ∈ 𝐴))
16	1, 15	bitrd 282	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143   ⊆ wss 3905  Ord word 6359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-ord 6363

This theorem is referenced by:  ontri1  6395  ordtri2  6396  ordtri4  6398  ordtr3  6407  ordintdif  6412  ordtri2or  6461  ordsucss  7810  ordsucsssuc  7815  ordsucuniel  7816  limsssuc  7842  ssnlim  7878  smoword  8349  tfrlem15  8375  nnaword  8609  nnawordex  8619  eldifsucnn  8646  nndomog  9193  onomeneq  9194  isfinite2  9254  unfilem1  9261  tfsnfin2  9316  wofib  9503  cantnflem1  9654  ttrcltr  9681  dmttrcl  9686  alephgeom  10062  alephdom2  10067  cflim2  10242  fin67  10374  winainflem  10673  finminlem  36829  ordeldif  43985  ordeldifsucon  43986  ordeldif1o  43987