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

Theorem soss 4348
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 4332 . . 3  |-  ( A 
C_  B  ->  ( R  Po  B  ->  R  Po  A ) )
2 ssel 3187 . . . . . . 7  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
3 ssel 3187 . . . . . . 7  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
42, 3anim12d 546 . . . . . 6  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  y  e.  A
)  ->  ( x  e.  B  /\  y  e.  B ) ) )
54imim1d 69 . . . . 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 1613 . . . 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 2593 . . . 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 2593 . . . 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 261 . . 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 546 . 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 4331 . 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 4331 . 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 261 1  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    \/ w3o 933   A.wal 1530    = wceq 1632    e. wcel 1696   A.wral 2556    C_ wss 3165   class class class wbr 4039    Po wpo 4328    Or wor 4329
This theorem is referenced by:  soeq2  4350  wess  4396  wereu  4405  wereu2  4406  ordunifi  7123  fisup2g  7233  fisupcl  7234  ordtypelem8  7256  wemapso2  7283  iunfictbso  7757  fin1a2lem10  8051  fin1a2lem11  8052  zornn0g  8148  ltsopi  8528  npomex  8636  fimaxre  9717  isercolllem1  12154  summolem2  12205  zsum  12207  gsumval3  15207  iccpnfhmeo  18459  xrhmeo  18460  dvgt0lem2  19366  dgrval  19626  dgrcl  19631  dgrub  19632  dgrlb  19634  aannenlem3  19726  logccv  20026  ssnnssfz  23292  xrge0iifiso  23332  erdszelem4  23740  erdszelem8  23744  erdsze2lem1  23749  erdsze2lem2  23750  supfz  24109  inffz  24110  prodmolem2  24158  zprod  24160  rencldnfilem  27006
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-in 3172  df-ss 3179  df-po 4330  df-so 4331
  Copyright terms: Public domain W3C validator