Theorem ordtri1 2970

Description: A trichotomy law for ordinals.

Assertion

Ref	Expression
ordtri1	|- ((Ord A /\ Ord B) -> (A (_ B <-> -. B e. A))

Proof of Theorem ordtri1

Step	Hyp	Ref	Expression
1		ordsseleq 2966	. 2 |- ((Ord A /\ Ord B) -> (A (_ B <-> (A e. B \/ A = B)))
2		ordn2lp 2958	. . . . 5 |- (Ord A -> -. (A e. B /\ B e. A))
3		imnan 242	. . . . 5 |- ((A e. B -> -. B e. A) <-> -. (A e. B /\ B e. A))
4	2, 3	sylibr 200	. . . 4 |- (Ord A -> (A e. B -> -. B e. A))
5		eleq2 1527	. . . . . 6 |- (A = B -> (B e. A <-> B e. B))
6	5	negbid 609	. . . . 5 |- (A = B -> (-. B e. A <-> -. B e. B))
7		ordirr 2956	. . . . 5 |- (Ord B -> -. B e. B)
8	6, 7	syl5cbir 211	. . . 4 |- (Ord B -> (A = B -> -. B e. A))
9	4, 8	jaao 427	. . 3 |- ((Ord A /\ Ord B) -> ((A e. B \/ A = B) -> -. B e. A))
10		ordtri3or 2969	. . . 4 |- ((Ord A /\ Ord B) -> (A e. B \/ A = B \/ B e. A))
11		df-3or 774	. . . . 5 |- ((A e. B \/ A = B \/ B e. A) <-> ((A e. B \/ A = B) \/ B e. A))
12		orcom 246	. . . . 5 |- (((A e. B \/ A = B) \/ B e. A) <-> (B e. A \/ (A e. B \/ A = B)))
13		df-or 224	. . . . 5 |- ((B e. A \/ (A e. B \/ A = B)) <-> (-. B e. A -> (A e. B \/ A = B)))
14	11, 12, 13	3bitr 177	. . . 4 |- ((A e. B \/ A = B \/ B e. A) <-> (-. B e. A -> (A e. B \/ A = B)))
15	10, 14	sylib 198	. . 3 |- ((Ord A /\ Ord B) -> (-. B e. A -> (A e. B \/ A = B)))
16	9, 15	impbid 514	. 2 |- ((Ord A /\ Ord B) -> ((A e. B \/ A = B) <-> -. B e. A))
17	1, 16	bitrd 526	1 |- ((Ord A /\ Ord B) -> (A (_ B <-> -. B e. A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   \/ w3o 772   = wceq 953   e. wcel 955   (_ wss 2037  Ord word 2937

This theorem is referenced by:  ontri1 2971  ordtri2 2972  ordtri4 2974  ordsucss 3059  ordsucsssuc 3064  limsssuc 3111  limom 3136  ssnlim 3157  oaabs 4236  onomeneq 4498  nndomo 4500  isfinite2 4523  unfilem1 4524  alephgeom 4854

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941

Copyright terms: Public domain