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

Theorem soss 4481
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 4465 . . 3  |-  ( A 
C_  B  ->  ( R  Po  B  ->  R  Po  A ) )
2 ssel 3302 . . . . . . 7  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
3 ssel 3302 . . . . . . 7  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
42, 3anim12d 547 . . . . . 6  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  y  e.  A
)  ->  ( x  e.  B  /\  y  e.  B ) ) )
54imim1d 71 . . . . 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 1630 . . . 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 2703 . . . 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 2703 . . . 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 262 . . 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 547 . 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 4464 . 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 4464 . 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 262 1  |-  ( A 
C_  B  ->  ( R  Or  B  ->  R  Or  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    \/ w3o 935   A.wal 1546    e. wcel 1721   A.wral 2666    C_ wss 3280   class class class wbr 4172    Po wpo 4461    Or wor 4462
This theorem is referenced by:  soeq2  4483  wess  4529  wereu  4538  wereu2  4539  ordunifi  7316  fisup2g  7427  fisupcl  7428  ordtypelem8  7450  wemapso2  7477  iunfictbso  7951  fin1a2lem10  8245  fin1a2lem11  8246  zornn0g  8341  ltsopi  8721  npomex  8829  fimaxre  9911  isercolllem1  12413  summolem2  12465  zsum  12467  gsumval3  15469  iccpnfhmeo  18923  xrhmeo  18924  dvgt0lem2  19840  dgrval  20100  dgrcl  20105  dgrub  20106  dgrlb  20108  aannenlem3  20200  logccv  20507  ssnnssfz  24101  xrge0iifiso  24274  erdszelem4  24833  erdszelem8  24837  erdsze2lem1  24842  erdsze2lem2  24843  supfz  25152  inffz  25153  prodmolem2  25214  zprod  25216  rencldnfilem  26771
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-in 3287  df-ss 3294  df-po 4463  df-so 4464
  Copyright terms: Public domain W3C validator