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

Theorem soss 5018
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 5002 . . 3 (𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))
2 ssel 3581 . . . . . . 7 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 ssel 3581 . . . . . . 7 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
42, 3anim12d 585 . . . . . 6 (𝐴𝐵 → ((𝑥𝐴𝑦𝐴) → (𝑥𝐵𝑦𝐵)))
54imim1d 82 . . . . 5 (𝐴𝐵 → (((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
652alimdv 1844 . . . 4 (𝐴𝐵 → (∀𝑥𝑦((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
7 r2al 2934 . . . 4 (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝑦((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
8 r2al 2934 . . . 4 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
96, 7, 83imtr4g 285 . . 3 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
101, 9anim12d 585 . 2 (𝐴𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
11 df-so 5001 . 2 (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
12 df-so 5001 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
1310, 11, 123imtr4g 285 1 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3o 1035  wal 1478  wcel 1987  wral 2907  wss 3559   class class class wbr 4618   Po wpo 4998   Or wor 4999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2912  df-in 3566  df-ss 3573  df-po 5000  df-so 5001
This theorem is referenced by:  soeq2  5020  wess  5066  wereu  5075  wereu2  5076  ordunifi  8162  fisup2g  8326  fisupcl  8327  fiinf2g  8358  ordtypelem8  8382  wemapso2lem  8409  iunfictbso  8889  fin1a2lem10  9183  fin1a2lem11  9184  zornn0g  9279  ltsopi  9662  npomex  9770  fimaxre  10920  suprfinzcl  11444  isercolllem1  14337  summolem2  14388  zsum  14390  prodmolem2  14601  zprod  14603  gsumval3  18240  iccpnfhmeo  22667  xrhmeo  22668  dvgt0lem2  23687  dgrval  23905  dgrcl  23910  dgrub  23911  dgrlb  23913  aannenlem3  24006  logccv  24326  xrge0infssd  29393  infxrge0lb  29396  infxrge0glb  29397  infxrge0gelb  29398  ssnnssfz  29414  xrge0iifiso  29787  omsfval  30161  omsf  30163  oms0  30164  omssubaddlem  30166  omssubadd  30167  oddpwdc  30221  erdszelem4  30919  erdszelem8  30923  erdsze2lem1  30928  erdsze2lem2  30929  supfz  31356  inffz  31357  inffzOLD  31358  nominmaxmo  31607  noprefixmo  31608  fin2so  33063  rencldnfilem  36899  fzisoeu  39009  fourierdlem36  39693  ssnn0ssfz  41441
  Copyright terms: Public domain W3C validator