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

Theorem soss 4818
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  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )

Proof of Theorem soss
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poss 4802 . . 3  |-  ( A 
C_  B  ->  ( R  Po  B  ->  R  Po  A ) )
2 ssel 3498 . . . . . . 7  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
3 ssel 3498 . . . . . . 7  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
42, 3anim12d 563 . . . . . 6  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  y  e.  A
)  ->  ( x  e.  B  /\  y  e.  B ) ) )
54imim1d 75 . . . . 5  |-  ( A 
C_  B  ->  (
( ( x  e.  B  /\  y  e.  B )  ->  (
x R y  \/  x  =  y  \/  y R x ) )  ->  ( (
x  e.  A  /\  y  e.  A )  ->  ( x R y  \/  x  =  y  \/  y R x ) ) ) )
652alimdv 1687 . . . 4  |-  ( A 
C_  B  ->  ( A. x A. y ( ( x  e.  B  /\  y  e.  B
)  ->  ( x R y  \/  x  =  y  \/  y R x ) )  ->  A. x A. y
( ( x  e.  A  /\  y  e.  A )  ->  (
x R y  \/  x  =  y  \/  y R x ) ) ) )
7 r2al 2842 . . . 4  |-  ( A. x  e.  B  A. y  e.  B  (
x R y  \/  x  =  y  \/  y R x )  <->  A. x A. y ( ( x  e.  B  /\  y  e.  B
)  ->  ( x R y  \/  x  =  y  \/  y R x ) ) )
8 r2al 2842 . . . 4  |-  ( A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x )  <->  A. x A. y ( ( x  e.  A  /\  y  e.  A
)  ->  ( x R y  \/  x  =  y  \/  y R x ) ) )
96, 7, 83imtr4g 270 . . 3  |-  ( A 
C_  B  ->  ( A. x  e.  B  A. y  e.  B  ( x R y  \/  x  =  y  \/  y R x )  ->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
101, 9anim12d 563 . 2  |-  ( A 
C_  B  ->  (
( R  Po  B  /\  A. x  e.  B  A. y  e.  B  ( x R y  \/  x  =  y  \/  y R x ) )  ->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) ) ) )
11 df-so 4801 . 2  |-  ( R  Or  B  <->  ( R  Po  B  /\  A. x  e.  B  A. y  e.  B  ( x R y  \/  x  =  y  \/  y R x ) ) )
12 df-so 4801 . 2  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
1310, 11, 123imtr4g 270 1  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    \/ w3o 972   A.wal 1377    e. wcel 1767   A.wral 2814    C_ wss 3476   class class class wbr 4447    Po wpo 4798    Or wor 4799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-in 3483  df-ss 3490  df-po 4800  df-so 4801
This theorem is referenced by:  soeq2  4820  wess  4866  wereu  4875  wereu2  4876  ordunifi  7766  fisup2g  7922  fisupcl  7923  ordtypelem8  7946  wemapso2OLD  7973  wemapso2lem  7974  iunfictbso  8491  fin1a2lem10  8785  fin1a2lem11  8786  zornn0g  8881  ltsopi  9262  npomex  9370  fimaxre  10486  suprfinzcl  10971  isercolllem1  13446  summolem2  13497  zsum  13499  gsumval3OLD  16699  gsumval3  16702  iccpnfhmeo  21180  xrhmeo  21181  dvgt0lem2  22139  dgrval  22360  dgrcl  22365  dgrub  22366  dgrlb  22368  aannenlem3  22460  logccv  22772  xrge0infssd  27249  ssnnssfz  27265  xrge0iifiso  27553  omsfval  27905  oms0  27906  oddpwdc  27933  erdszelem4  28278  erdszelem8  28282  erdsze2lem1  28287  erdsze2lem2  28288  supfz  28582  inffz  28583  prodmolem2  28644  zprod  28646  fin2so  29617  rencldnfilem  30358  fzisoeu  31077  fourierdlem36  31443  fourierdlem54  31461  ssnn0ssfz  32002
  Copyright terms: Public domain W3C validator