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

Theorem soss 4808
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 4792 . . 3  |-  ( A 
C_  B  ->  ( R  Po  B  ->  R  Po  A ) )
2 ssel 3483 . . . . . . 7  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
3 ssel 3483 . . . . . . 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 1698 . . . 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 2821 . . . 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 2821 . . . 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 4791 . 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 4791 . 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 973   A.wal 1381    e. wcel 1804   A.wral 2793    C_ wss 3461   class class class wbr 4437    Po wpo 4788    Or wor 4789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-ral 2798  df-in 3468  df-ss 3475  df-po 4790  df-so 4791
This theorem is referenced by:  soeq2  4810  wess  4856  wereu  4865  wereu2  4866  ordunifi  7772  fisup2g  7929  fisupcl  7930  ordtypelem8  7953  wemapso2OLD  7980  wemapso2lem  7981  iunfictbso  8498  fin1a2lem10  8792  fin1a2lem11  8793  zornn0g  8888  ltsopi  9269  npomex  9377  fimaxre  10496  suprfinzcl  10983  isercolllem1  13466  summolem2  13517  zsum  13519  gsumval3OLD  16782  gsumval3  16785  iccpnfhmeo  21318  xrhmeo  21319  dvgt0lem2  22277  dgrval  22498  dgrcl  22503  dgrub  22504  dgrlb  22506  aannenlem3  22598  logccv  22916  xrge0infssd  27453  ssnnssfz  27469  xrge0iifiso  27790  omsfval  28138  oms0  28139  oddpwdc  28166  erdszelem4  28511  erdszelem8  28515  erdsze2lem1  28520  erdsze2lem2  28521  supfz  28980  inffz  28981  prodmolem2  29042  zprod  29044  fin2so  30015  rencldnfilem  30729  fzisoeu  31449  fourierdlem36  31814  ssnn0ssfz  32671
  Copyright terms: Public domain W3C validator