Theorem fss 3635

Description: Expanding the codomain of a mapping.

Assertion

Ref	Expression
fss	|- ((F:A-->B /\ B (_ C) -> F:A-->C)

Proof of Theorem fss

Step	Hyp	Ref	Expression
1		ffn 3627	. . . 4 |- (F:A-->B -> F Fn A)
2	1	adantr 389	. . 3 |- ((F:A-->B /\ B (_ C) -> F Fn A)
3		frn 3633	. . . . 5 |- (F:A-->B -> ran F (_ B)
4		sstr2 2071	. . . . 5 |- (ran F (_ B -> (B (_ C -> ran F (_ C))
5	3, 4	syl 10	. . . 4 |- (F:A-->B -> (B (_ C -> ran F (_ C))
6	5	imp 350	. . 3 |- ((F:A-->B /\ B (_ C) -> ran F (_ C)
7	2, 6	jca 288	. 2 |- ((F:A-->B /\ B (_ C) -> (F Fn A /\ ran F (_ C))
8		df-f 3194	. 2 |- (F:A-->C <-> (F Fn A /\ ran F (_ C))
9	7, 8	sylibr 200	1 |- ((F:A-->B /\ B (_ C) -> F:A-->C)

Syntax hints:   -> wi 3   /\ wa 223   (_ wss 2047  ran crn 3171   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  ffoss 3711  fsn2 3836  map0 4344  mapsn 4345  mapss 4346  ssdomg 4408  ac6lem 4754  ac6s 4756  alephfplem4 4899  uzrdgfnuz 6306  ser1mono 6337  seq1ublem 6911  ser1absdiflem 6929  climserzle 7147  climsup 7155  caucvglem2 7158  caucvg 7163  caucvg3t 7168  ser1clim0 7173  ser1cmp0 7175  cvgcmp2clem 7182  cvgcmp3c 7186  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  cncffvrn 7273  abscncflem 7274  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  ruclem39 7548  infmap2lem2 7580  cnconst 7780  metcnss 7898  lmconst 7934  lmss 7953  causs 7955  metelcls 7965  bcthlem33 8031  bcth 8032  0oo 8449  ubthlem3 8531  ubthi 8544  hlim0 9105  hhsscms 9150  projlem26 9211  projlem29 9214  osumlem4 9581  pjft 9653  0cnfn 9904  0lnfn 9909  pjinvar 10119

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053  df-f 3194

Copyright terms: Public domain