Theorem fss 5419

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 3190	. . . . 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 5262	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5		df-f 5262	. . 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 3157   ran crn 4664   Fn wfn 5253   -->wf 5254

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-f 5262

This theorem is referenced by:  fssd  5420  fconst6g  5456  f1ss  5469  ffoss  5536  fsn2  5736  ofco  6154  tposf2  6326  issmo2  6347  smoiso  6360  mapsn  6749  ssdomg  6837  omp1eomlem  7160  1fv  10214  fxnn0nninf  10531  abscn2  11480  recn2  11482  imcn2  11483  climabs  11485  climre  11487  climim  11488  fsumre  11637  fsumim  11638  resmhm2  13120  ismet2  14590  dvfre  14946  dvrecap  14949  elplyr  14976  lgsfcl  15249