Theorem fss 5527

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 3249	. . . . 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 5362	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5		df-f 5362	. . 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 3214   ran crn 4756   Fn wfn 5353   -->wf 5354

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-f 5362

This theorem is referenced by:  fssd  5528  fconst6g  5572  f1ss  5585  ffoss  5653  fsn2  5857  ofco  6295  tposf2  6513  issmo2  6534  smoiso  6547  mapsn  6939  ssdomg  7032  omp1eomlem  7399  1fv  10499  fxnn0nninf  10829  abscn2  12030  recn2  12032  imcn2  12033  climabs  12035  climre  12037  climim  12038  fsumre  12188  fsumim  12189  resmhm2  13748  prdsgrpd  14144  prdsinvgd  14145  ismet2  15350  dvfre  15706  dvrecap  15709  elplyr  15736  lgsfcl  16012  konigsbergssiedgwen  16612