Theorem fss 3632

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 3624	. . . 4 |- (F:A-->B -> F Fn A)
2	1	adantr 389	. . 3 |- ((F:A-->B /\ B (_ C) -> F Fn A)
3		frn 3630	. . . . 5 |- (F:A-->B -> ran F (_ B)
4		sstr2 2069	. . . . 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 3191	. 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 2045  ran crn 3168   Fn wfn 3174  -->wf 3175

This theorem is referenced by:  ffoss 3708  fsn2 3833  map0 4341  mapsn 4342  mapss 4343  ssdomg 4402  ac6lem 4741  ac6s 4743  alephfplem4 4886  uzrdgfnuz 6261  ser1mono 6292  seq1ublem 6877  ser1absdiflem 6895  climserzle 7116  climsup 7124  caucvglem2 7127  caucvg 7132  caucvg3t 7139  ser1clim0 7144  ser1cmp0 7146  cvgcmp2clem 7153  cvgcmp3c 7157  cvgcmp3cetlem1 7159  cvgcmp3cetlem2 7160  cncffvrn 7244  abscncflem 7245  acdc3lem 7464  acdc2lem2 7467  acdc5lem2 7470  acdclem 7472  ruclem39 7527  infmap2lem2 7559  cnconst 7759  metcnss 7881  lmconst 7917  lmss 7936  causs 7938  metelcls 7948  bcthlem33 8014  bcth 8015  0oo 8434  ubthlem3 8515  ubthi 8528  hlim0 9093  hhsscms 9138  projlem26 9199  projlem29 9202  osumlem4 9571  pjft 9644  0cnfn 9895  0lnfn 9900  pjinvar 10110

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

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

Copyright terms: Public domain