Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  soss Structured version   Visualization version   GIF version

Theorem soss 5488
 Description: Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
soss (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))

Proof of Theorem soss
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poss 5471 . . 3 (𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))
2 ss2ralv 4035 . . 3 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
31, 2anim12d 610 . 2 (𝐴𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
4 df-so 5470 . 2 (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
5 df-so 5470 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
63, 4, 53imtr4g 298 1 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∨ w3o 1082  ∀wral 3138   ⊆ wss 3936   class class class wbr 5059   Po wpo 5467   Or wor 5468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-in 3943  df-ss 3952  df-po 5469  df-so 5470 This theorem is referenced by:  soeq2  5490  wess  5537  wereu  5546  wereu2  5547  ordunifi  8762  fisup2g  8926  fisupcl  8927  fiinf2g  8958  ordtypelem8  8983  wemapso2lem  9010  iunfictbso  9534  fin1a2lem10  9825  fin1a2lem11  9826  zornn0g  9921  ltsopi  10304  npomex  10412  fimaxre  11578  fimaxreOLD  11579  fiminre  11582  suprfinzcl  12091  isercolllem1  15015  summolem2  15067  zsum  15069  prodmolem2  15283  zprod  15285  gsumval3  19021  iccpnfhmeo  23543  xrhmeo  23544  dvgt0lem2  24594  dgrval  24812  dgrcl  24817  dgrub  24818  dgrlb  24820  aannenlem3  24913  logccv  25240  xrge0infssd  30479  infxrge0lb  30482  infxrge0glb  30483  infxrge0gelb  30484  ssnnssfz  30504  xrge0iifiso  31173  omsfval  31547  omsf  31549  oms0  31550  omssubaddlem  31552  omssubadd  31553  oddpwdc  31607  erdszelem4  32436  erdszelem8  32440  erdsze2lem1  32445  erdsze2lem2  32446  supfz  32955  inffz  32956  nomaxmo  33196  finorwe  34657  fin2so  34873  rencldnfilem  39410  fzisoeu  41559  fourierdlem36  42421  ssnn0ssfz  44390
 Copyright terms: Public domain W3C validator