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

Theorem funss 5586
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 4910 . . 3  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )
2 coss1 4978 . . . . 5  |-  ( A 
C_  B  ->  ( A  o.  `' A
)  C_  ( B  o.  `' A ) )
3 cnvss 4995 . . . . . 6  |-  ( A 
C_  B  ->  `' A  C_  `' B )
4 coss2 4979 . . . . . 6  |-  ( `' A  C_  `' B  ->  ( B  o.  `' A )  C_  ( B  o.  `' B
) )
53, 4syl 17 . . . . 5  |-  ( A 
C_  B  ->  ( B  o.  `' A
)  C_  ( B  o.  `' B ) )
62, 5sstrd 3451 . . . 4  |-  ( A 
C_  B  ->  ( A  o.  `' A
)  C_  ( B  o.  `' B ) )
7 sstr2 3448 . . . 4  |-  ( ( A  o.  `' A
)  C_  ( B  o.  `' B )  ->  (
( B  o.  `' B )  C_  _I  ->  ( A  o.  `' A )  C_  _I  ) )
86, 7syl 17 . . 3  |-  ( A 
C_  B  ->  (
( B  o.  `' B )  C_  _I  ->  ( A  o.  `' A )  C_  _I  ) )
91, 8anim12d 561 . 2  |-  ( A 
C_  B  ->  (
( Rel  B  /\  ( B  o.  `' B )  C_  _I  )  ->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) ) )
10 df-fun 5570 . 2  |-  ( Fun 
B  <->  ( Rel  B  /\  ( B  o.  `' B )  C_  _I  ) )
11 df-fun 5570 . 2  |-  ( Fun 
A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
129, 10, 113imtr4g 270 1  |-  ( A 
C_  B  ->  ( Fun  B  ->  Fun  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    C_ wss 3413    _I cid 4732   `'ccnv 4821    o. ccom 4826   Rel wrel 4827   Fun wfun 5562
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 3420  df-ss 3427  df-br 4395  df-opab 4453  df-rel 4829  df-cnv 4830  df-co 4831  df-fun 5570
This theorem is referenced by:  funeq  5587  funopab4  5603  funres  5607  fun0  5625  funcnvcnv  5626  funin  5635  funres11  5636  foimacnv  5815  funsssuppss  6928  strssd  14877  strle1  14938  xpsc0  15172  xpsc1  15173  pjpm  19035  frrlem5c  30080
  Copyright terms: Public domain W3C validator