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

Theorem soss 5612
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 5594 . . 3 (𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))
2 ss2ralv 4054 . . 3 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
31, 2anim12d 609 . 2 (𝐴𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
4 df-so 5593 . 2 (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
5 df-so 5593 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
63, 4, 53imtr4g 296 1 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3o 1086  wral 3061  wss 3951   class class class wbr 5143   Po wpo 5590   Or wor 5591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3062  df-ss 3968  df-po 5592  df-so 5593
This theorem is referenced by:  soeq2  5614  wess  5671  wereu  5681  wereu2  5682  ordunifi  9326  fisup2g  9508  fisupcl  9509  fiinf2g  9540  ordtypelem8  9565  wemapso2lem  9592  iunfictbso  10154  fin1a2lem10  10449  fin1a2lem11  10450  zornn0g  10545  ltsopi  10928  npomex  11036  fimaxre  12212  fiminre  12215  suprfinzcl  12732  isercolllem1  15701  summolem2  15752  zsum  15754  prodmolem2  15971  zprod  15973  gsumval3  19925  iccpnfhmeo  24976  xrhmeo  24977  dvgt0lem2  26042  dgrval  26267  dgrcl  26272  dgrub  26273  dgrlb  26275  aannenlem3  26372  logccv  26705  nomaxmo  27743  nominmo  27744  xrge0infssd  32765  infxrge0lb  32768  infxrge0glb  32769  infxrge0gelb  32770  ssnnssfz  32789  xrge0iifiso  33934  omsfval  34296  omsf  34298  oms0  34299  omssubaddlem  34301  omssubadd  34302  oddpwdc  34356  erdszelem4  35199  erdszelem8  35203  erdsze2lem1  35208  erdsze2lem2  35209  supfz  35729  inffz  35730  finorwe  37383  fin2so  37614  sticksstones3  42149  rencldnfilem  42831  fzisoeu  45312  fourierdlem36  46158  ssnn0ssfz  48265
  Copyright terms: Public domain W3C validator