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

Theorem soss 4664
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 4648 . . 3  |-  ( A 
C_  B  ->  ( R  Po  B  ->  R  Po  A ) )
2 ssel 3355 . . . . . . 7  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
3 ssel 3355 . . . . . . 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 1677 . . . 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 2757 . . . 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 2757 . . . 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 4647 . 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 4647 . 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 964   A.wal 1367    e. wcel 1756   A.wral 2720    C_ wss 3333   class class class wbr 4297    Po wpo 4644    Or wor 4645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-in 3340  df-ss 3347  df-po 4646  df-so 4647
This theorem is referenced by:  soeq2  4666  wess  4712  wereu  4721  wereu2  4722  ordunifi  7567  fisup2g  7721  fisupcl  7722  ordtypelem8  7744  wemapso2OLD  7771  wemapso2lem  7772  iunfictbso  8289  fin1a2lem10  8583  fin1a2lem11  8584  zornn0g  8679  ltsopi  9062  npomex  9170  fimaxre  10282  isercolllem1  13147  summolem2  13198  zsum  13200  gsumval3OLD  16387  gsumval3  16390  iccpnfhmeo  20522  xrhmeo  20523  dvgt0lem2  21480  dgrval  21701  dgrcl  21706  dgrub  21707  dgrlb  21709  aannenlem3  21801  logccv  22113  xrge0infssd  26059  ssnnssfz  26081  xrge0iifiso  26370  omsfval  26714  oms0  26715  oddpwdc  26742  erdszelem4  27087  erdszelem8  27091  erdsze2lem1  27096  erdsze2lem2  27097  supfz  27391  inffz  27392  prodmolem2  27453  zprod  27455  fin2so  28421  rencldnfilem  29164  ssnn0ssfz  30746  suprfinzcl  30750
  Copyright terms: Public domain W3C validator