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

Theorem funss 5275
Description: Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
Assertion
Ref Expression
funss  |-  ( A 
C_  B  ->  ( Fun  B  ->  Fun  A ) )

Proof of Theorem funss
StepHypRef Expression
1 relss 4777 . . 3  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )
2 coss1 4841 . . . . 5  |-  ( A 
C_  B  ->  ( A  o.  `' A
)  C_  ( B  o.  `' A ) )
3 cnvss 4856 . . . . . 6  |-  ( A 
C_  B  ->  `' A  C_  `' B )
4 coss2 4842 . . . . . 6  |-  ( `' A  C_  `' B  ->  ( B  o.  `' A )  C_  ( B  o.  `' B
) )
53, 4syl 15 . . . . 5  |-  ( A 
C_  B  ->  ( B  o.  `' A
)  C_  ( B  o.  `' B ) )
62, 5sstrd 3191 . . . 4  |-  ( A 
C_  B  ->  ( A  o.  `' A
)  C_  ( B  o.  `' B ) )
7 sstr2 3188 . . . 4  |-  ( ( A  o.  `' A
)  C_  ( B  o.  `' B )  ->  (
( B  o.  `' B )  C_  _I  ->  ( A  o.  `' A )  C_  _I  ) )
86, 7syl 15 . . 3  |-  ( A 
C_  B  ->  (
( B  o.  `' B )  C_  _I  ->  ( A  o.  `' A )  C_  _I  ) )
91, 8anim12d 546 . 2  |-  ( A 
C_  B  ->  (
( Rel  B  /\  ( B  o.  `' B )  C_  _I  )  ->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) ) )
10 df-fun 5259 . 2  |-  ( Fun 
B  <->  ( Rel  B  /\  ( B  o.  `' B )  C_  _I  ) )
11 df-fun 5259 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
129, 10, 113imtr4g 261 1  |-  ( A 
C_  B  ->  ( Fun  B  ->  Fun  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3154    _I cid 4306   `'ccnv 4690    o. ccom 4695   Rel wrel 4696   Fun wfun 5251
This theorem is referenced by:  funeq  5276  funopab4  5291  funres  5295  fun0  5309  funcnvcnv  5310  funin  5321  funres11  5322  foimacnv  5492  strssd  13184  strle1  13241  xpsc0  13464  xpsc1  13465  pjpm  16610  frrlem5c  24289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-in 3161  df-ss 3168  df-br 4026  df-opab 4080  df-rel 4698  df-cnv 4699  df-co 4700  df-fun 5259
  Copyright terms: Public domain W3C validator