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

Theorem soss 5281
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 5265 . . 3 (𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))
2 ssel 3821 . . . . . . 7 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 ssel 3821 . . . . . . 7 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
42, 3anim12d 602 . . . . . 6 (𝐴𝐵 → ((𝑥𝐴𝑦𝐴) → (𝑥𝐵𝑦𝐵)))
54imim1d 82 . . . . 5 (𝐴𝐵 → (((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
652alimdv 2017 . . . 4 (𝐴𝐵 → (∀𝑥𝑦((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
7 r2al 3148 . . . 4 (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝑦((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
8 r2al 3148 . . . 4 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
96, 7, 83imtr4g 288 . . 3 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
101, 9anim12d 602 . 2 (𝐴𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
11 df-so 5264 . 2 (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
12 df-so 5264 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
1310, 11, 123imtr4g 288 1 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3o 1110  wal 1654  wcel 2164  wral 3117  wss 3798   class class class wbr 4873   Po wpo 5261   Or wor 5262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-ral 3122  df-in 3805  df-ss 3812  df-po 5263  df-so 5264
This theorem is referenced by:  soeq2  5283  wess  5329  wereu  5338  wereu2  5339  ordunifi  8479  fisup2g  8643  fisupcl  8644  fiinf2g  8675  ordtypelem8  8699  wemapso2lem  8726  iunfictbso  9250  fin1a2lem10  9546  fin1a2lem11  9547  zornn0g  9642  ltsopi  10025  npomex  10133  fimaxre  11298  suprfinzcl  11820  isercolllem1  14772  summolem2  14824  zsum  14826  prodmolem2  15038  zprod  15040  gsumval3  18661  iccpnfhmeo  23114  xrhmeo  23115  dvgt0lem2  24165  dgrval  24383  dgrcl  24388  dgrub  24389  dgrlb  24391  aannenlem3  24484  logccv  24808  xrge0infssd  30062  infxrge0lb  30065  infxrge0glb  30066  infxrge0gelb  30067  ssnnssfz  30085  xrge0iifiso  30515  omsfval  30890  omsf  30892  oms0  30893  omssubaddlem  30895  omssubadd  30896  oddpwdc  30950  erdszelem4  31711  erdszelem8  31715  erdsze2lem1  31720  erdsze2lem2  31721  supfz  32145  inffz  32146  nomaxmo  32375  fin2so  33932  rencldnfilem  38221  fzisoeu  40305  fourierdlem36  41147  ssnn0ssfz  42967
  Copyright terms: Public domain W3C validator