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

Theorem coss2 4980
Description: Subclass theorem for composition. (Contributed by NM, 5-Apr-2013.)
Assertion
Ref Expression
coss2  |-  ( A 
C_  B  ->  ( C  o.  A )  C_  ( C  o.  B
) )

Proof of Theorem coss2
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . 6  |-  ( A 
C_  B  ->  A  C_  B )
21ssbrd 4436 . . . . 5  |-  ( A 
C_  B  ->  (
x A y  ->  x B y ) )
32anim1d 562 . . . 4  |-  ( A 
C_  B  ->  (
( x A y  /\  y C z )  ->  ( x B y  /\  y C z ) ) )
43eximdv 1731 . . 3  |-  ( A 
C_  B  ->  ( E. y ( x A y  /\  y C z )  ->  E. y
( x B y  /\  y C z ) ) )
54ssopab2dv 4719 . 2  |-  ( A 
C_  B  ->  { <. x ,  z >.  |  E. y ( x A y  /\  y C z ) }  C_  {
<. x ,  z >.  |  E. y ( x B y  /\  y C z ) } )
6 df-co 4832 . 2  |-  ( C  o.  A )  =  { <. x ,  z
>.  |  E. y
( x A y  /\  y C z ) }
7 df-co 4832 . 2  |-  ( C  o.  B )  =  { <. x ,  z
>.  |  E. y
( x B y  /\  y C z ) }
85, 6, 73sstr4g 3483 1  |-  ( A 
C_  B  ->  ( C  o.  A )  C_  ( C  o.  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   E.wex 1633    C_ wss 3414   class class class wbr 4395   {copab 4452    o. ccom 4827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-in 3421  df-ss 3428  df-br 4396  df-opab 4454  df-co 4832
This theorem is referenced by:  coeq2  4982  funss  5587  tposss  6959  dftpos4  6977  rtrclreclem4  13043  tsrdir  16192  mvdco  16794  ustex2sym  21011  ustex3sym  21012  ustund  21016  ustneism  21018  trust  21024  utop2nei  21045  neipcfilu  21091  fcoinver  27896  trrelsuperrel2dg  35650
  Copyright terms: Public domain W3C validator