Theorem fss 5549

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 3255	. . . . 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 5384	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5		df-f 5384	. . 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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   C_ wss 3220   ran crn 4777   Fn wfn 5375   -->wf 5376

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5384

This theorem is used by:  fssd  5550  fconst6g  5594  f1ss  5607  ffoss  5675  fsn2  5885  ofco  6325  tposf2  6543  issmo2  6564  smoiso  6577  mapsn  6976  ssdomg  7069  omp1eomlem  7440  1fv  10563  fxnn0nninf  10897  hashf1lem1  11307  abscn2  12106  recn2  12108  imcn2  12109  climabs  12111  climre  12113  climim  12114  fsumre  12264  fsumim  12265  resmhm2  13854  prdsgrpd  14304  prdsinvgd  14305  psrridmfi  15200  ismet2  15580  dvfre  15936  dvrecap  15939  elplyr  15966  lgsfcl  16332  konigsbergssiedgwen  16932