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  6254  tposf2  6434  issmo2  6455  smoiso  6468  mapsn  6859  ssdomg  6952  omp1eomlem  7293  1fv  10374  fxnn0nninf  10702  abscn2  11893  recn2  11895  imcn2  11896  climabs  11898  climre  11900  climim  11901  fsumre  12051  fsumim  12052  resmhm2  13589  prdsgrpd  13710  prdsinvgd  13711  ismet2  15097  dvfre  15453  dvrecap  15456  elplyr  15483  lgsfcl  15756  konigsbergssiedgwen  16356