Theorem fss 5494

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 3234	. . . . 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 5330	. . 3 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
5		df-f 5330	. . 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 3200   ran crn 4726   Fn wfn 5321   -->wf 5322

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-f 5330

This theorem is referenced by:  fssd  5495  fconst6g  5535  f1ss  5548  ffoss  5616  fsn2  5821  ofco  6253  tposf2  6433  issmo2  6454  smoiso  6467  mapsn  6858  ssdomg  6951  omp1eomlem  7292  1fv  10373  fxnn0nninf  10700  abscn2  11875  recn2  11877  imcn2  11878  climabs  11880  climre  11882  climim  11883  fsumre  12032  fsumim  12033  resmhm2  13570  prdsgrpd  13691  prdsinvgd  13692  ismet2  15077  dvfre  15433  dvrecap  15436  elplyr  15463  lgsfcl  15736