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

Theorem soss 4823
 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

Proof of Theorem soss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poss 4807 . . 3
2 ssel 3497 . . . . . . 7
3 ssel 3497 . . . . . . 7
42, 3anim12d 563 . . . . . 6
54imim1d 75 . . . . 5
652alimdv 1711 . . . 4
7 r2al 2835 . . . 4
8 r2al 2835 . . . 4
96, 7, 83imtr4g 270 . . 3
101, 9anim12d 563 . 2
11 df-so 4806 . 2
12 df-so 4806 . 2
1310, 11, 123imtr4g 270 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  \/w3o 972  A.wal 1393  e.wcel 1818  A.wral 2807  C_wss 3475   class class class wbr 4452  Powpo 4803  Orwor 4804 This theorem is referenced by:  soeq2  4825  wess  4871  wereu  4880  wereu2  4881  ordunifi  7790  fisup2g  7947  fisupcl  7948  ordtypelem8  7971  wemapso2OLD  7998  wemapso2lem  7999  iunfictbso  8516  fin1a2lem10  8810  fin1a2lem11  8811  zornn0g  8906  ltsopi  9287  npomex  9395  fimaxre  10515  suprfinzcl  11003  isercolllem1  13487  summolem2  13538  zsum  13540  prodmolem2  13742  zprod  13744  gsumval3OLD  16908  gsumval3  16911  iccpnfhmeo  21445  xrhmeo  21446  dvgt0lem2  22404  dgrval  22625  dgrcl  22630  dgrub  22631  dgrlb  22633  aannenlem3  22726  logccv  23044  xrge0infssd  27581  ssnnssfz  27597  xrge0iifiso  27917  omsfval  28265  oms0  28266  oddpwdc  28293  erdszelem4  28638  erdszelem8  28642  erdsze2lem1  28647  erdsze2lem2  28648  supfz  29107  inffz  29108  fin2so  30040  rencldnfilem  30754  fzisoeu  31500  fourierdlem36  31925  ssnn0ssfz  32938 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-in 3482  df-ss 3489  df-po 4805  df-so 4806
 Copyright terms: Public domain W3C validator