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

Theorem soss 5605
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 5587 . . 3 (𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))
2 ss2ralv 4049 . . 3 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
31, 2anim12d 608 . 2 (𝐴𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
4 df-so 5586 . 2 (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
5 df-so 5586 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
63, 4, 53imtr4g 296 1 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3o 1084  wral 3057  wss 3945   class class class wbr 5143   Po wpo 5583   Or wor 5584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3058  df-v 3472  df-in 3952  df-ss 3962  df-po 5585  df-so 5586
This theorem is referenced by:  soeq2  5607  wess  5660  wereu  5669  wereu2  5670  ordunifi  9312  fisup2g  9486  fisupcl  9487  fiinf2g  9518  ordtypelem8  9543  wemapso2lem  9570  iunfictbso  10132  fin1a2lem10  10427  fin1a2lem11  10428  zornn0g  10523  ltsopi  10906  npomex  11014  fimaxre  12183  fiminre  12186  suprfinzcl  12701  isercolllem1  15638  summolem2  15689  zsum  15691  prodmolem2  15906  zprod  15908  gsumval3  19856  iccpnfhmeo  24864  xrhmeo  24865  dvgt0lem2  25930  dgrval  26156  dgrcl  26161  dgrub  26162  dgrlb  26164  aannenlem3  26259  logccv  26591  nomaxmo  27625  nominmo  27626  xrge0infssd  32526  infxrge0lb  32529  infxrge0glb  32530  infxrge0gelb  32531  ssnnssfz  32550  xrge0iifiso  33531  omsfval  33909  omsf  33911  oms0  33912  omssubaddlem  33914  omssubadd  33915  oddpwdc  33969  erdszelem4  34799  erdszelem8  34803  erdsze2lem1  34808  erdsze2lem2  34809  supfz  35318  inffz  35319  finorwe  36856  fin2so  37075  sticksstones3  41615  rencldnfilem  42231  fzisoeu  44673  fourierdlem36  45522  ssnn0ssfz  47404
  Copyright terms: Public domain W3C validator