Theorem ordtri1 6379

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 6375	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
2		ordn2lp 6366	. . . . 5 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
3		imnan 403	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
4	2, 3	sylibr 236	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴))
5		ordirr 6364	. . . . 5 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
6		eleq2 2851	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵))
7	6	notbid 320	. . . . 5 ⊢ (𝐴 = 𝐵 → (¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵))
8	5, 7	syl5ibrcom 249	. . . 4 ⊢ (Ord 𝐵 → (𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴))
9	4, 8	jaao 967	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) → ¬ 𝐵 ∈ 𝐴))
10		ordtri3or 6378	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
11		df-3or 1099	. . . . . 6 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ∨ 𝐵 ∈ 𝐴))
12	10, 11	sylib 220	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ∨ 𝐵 ∈ 𝐴))
13	12	orcomd 882	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ∨ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
14	13	ord 875	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ 𝐵 ∈ 𝐴 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
15	9, 14	impbid 214	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ↔ ¬ 𝐵 ∈ 𝐴))
16	1, 15	bitrd 281	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∨ w3o 1097   = wceq 1560   ∈ wcel 2142   ⊆ wss 3904  Ord word 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-ord 6349

This theorem is referenced by:  ontri1  6380  ordtri2  6381  ordtri4  6383  ordtr3  6392  ordintdif  6397  ordtri2or  6446  ordsucss  7798  ordsucsssuc  7803  ordsucuniel  7804  limsssuc  7830  ssnlim  7866  smoword  8337  tfrlem15  8363  nnaword  8597  nnawordex  8607  eldifsucnn  8634  nndomog  9181  onomeneq  9182  isfinite2  9242  unfilem1  9249  tfsnfin2  9306  wofib  9493  cantnflem1  9644  ttrcltr  9671  dmttrcl  9676  alephgeom  10038  alephdom2  10043  cflim2  10220  fin67  10352  winainflem  10651  finminlem  36675  ordeldif  43832  ordeldifsucon  43833  ordeldif1o  43834