Theorem fss 5349

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 3149	. . . . 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 335	. . 3 |- ( B C_ C -> ( ( F Fn A /\ ran F C_ B ) -> ( F Fn A /\ ran F C_ C ) ) )
4		df-f 5192	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5		df-f 5192	. . 3 |- ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
6	3, 4, 5	3imtr4g 204	. 2 |- ( B C_ C -> ( F : A --> B -> F : A --> C ) )
7	6	impcom 124	1 |- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )

Syntax hints:   -> wi 4   /\ wa 103   C_ wss 3116   ran crn 4605   Fn wfn 5183   -->wf 5184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129  df-f 5192

This theorem is referenced by:  fssd  5350  fconst6g  5386  f1ss  5399  ffoss  5464  fsn2  5659  ofco  6068  tposf2  6236  issmo2  6257  smoiso  6270  mapsn  6656  ssdomg  6744  omp1eomlem  7059  1fv  10074  fxnn0nninf  10373  abscn2  11256  recn2  11258  imcn2  11259  climabs  11261  climre  11263  climim  11264  fsumre  11413  fsumim  11414  ismet2  12994  dvfre  13314  dvrecap  13317  lgsfcl  13549