Theorem fss 5437

Description: Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Assertion

Ref	Expression
fss	|- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )

Proof of Theorem fss

Step	Hyp	Ref	Expression
1		sstr2 3200	. . . . 5 |- ( ran F C_ B -> ( B C_ C -> ran F C_ C ) )
2	1	com12 30	. . . 4 |- ( B C_ C -> ( ran F C_ B -> ran F C_ C ) )
3	2	anim2d 337	. . 3 |- ( B C_ C -> ( ( F Fn A /\ ran F C_ B ) -> ( F Fn A /\ ran F C_ C ) ) )
4		df-f 5275	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5		df-f 5275	. . 3 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
6	3, 4, 5	3imtr4g 205	. 2 |- ( B C_ C -> ( F : A --> B -> F : A --> C ) )
7	6	impcom 125	1 |- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )

Syntax hints:   -> wi 4   /\ wa 104   C_ wss 3166   ran crn 4676   Fn wfn 5266   -->wf 5267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179  df-f 5275

This theorem is referenced by:  fssd  5438  fconst6g  5474  f1ss  5487  ffoss  5554  fsn2  5754  ofco  6177  tposf2  6354  issmo2  6375  smoiso  6388  mapsn  6777  ssdomg  6870  omp1eomlem  7196  1fv  10261  fxnn0nninf  10584  abscn2  11626  recn2  11628  imcn2  11629  climabs  11631  climre  11633  climim  11634  fsumre  11783  fsumim  11784  resmhm2  13320  prdsgrpd  13441  prdsinvgd  13442  ismet2  14826  dvfre  15182  dvrecap  15185  elplyr  15212  lgsfcl  15485