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

Theorem soss 5566
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 5548 . . 3 (𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))
2 ss2ralv 4013 . . 3 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
31, 2anim12d 610 . 2 (𝐴𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
4 df-so 5547 . 2 (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
5 df-so 5547 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
63, 4, 53imtr4g 296 1 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3o 1087  wral 3065  wss 3911   class class class wbr 5106   Po wpo 5544   Or wor 5545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-v 3448  df-in 3918  df-ss 3928  df-po 5546  df-so 5547
This theorem is referenced by:  soeq2  5568  wess  5621  wereu  5630  wereu2  5631  ordunifi  9238  fisup2g  9405  fisupcl  9406  fiinf2g  9437  ordtypelem8  9462  wemapso2lem  9489  iunfictbso  10051  fin1a2lem10  10346  fin1a2lem11  10347  zornn0g  10442  ltsopi  10825  npomex  10933  fimaxre  12100  fiminre  12103  suprfinzcl  12618  isercolllem1  15550  summolem2  15602  zsum  15604  prodmolem2  15819  zprod  15821  gsumval3  19685  iccpnfhmeo  24311  xrhmeo  24312  dvgt0lem2  25370  dgrval  25592  dgrcl  25597  dgrub  25598  dgrlb  25600  aannenlem3  25693  logccv  26021  nomaxmo  27049  nominmo  27050  xrge0infssd  31669  infxrge0lb  31672  infxrge0glb  31673  infxrge0gelb  31674  ssnnssfz  31693  xrge0iifiso  32519  omsfval  32897  omsf  32899  oms0  32900  omssubaddlem  32902  omssubadd  32903  oddpwdc  32957  erdszelem4  33791  erdszelem8  33795  erdsze2lem1  33800  erdsze2lem2  33801  supfz  34304  inffz  34305  finorwe  35856  fin2so  36068  sticksstones3  40559  rencldnfilem  41146  fzisoeu  43541  fourierdlem36  44391  ssnn0ssfz  46432
  Copyright terms: Public domain W3C validator