ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fss Unicode version

Theorem fss 5085
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
StepHypRef Expression
1 sstr2 3007 . . . . 5  |-  ( ran 
F  C_  B  ->  ( B  C_  C  ->  ran 
F  C_  C )
)
21com12 30 . . . 4  |-  ( B 
C_  C  ->  ( ran  F  C_  B  ->  ran 
F  C_  C )
)
32anim2d 330 . . 3  |-  ( B 
C_  C  ->  (
( F  Fn  A  /\  ran  F  C_  B
)  ->  ( F  Fn  A  /\  ran  F  C_  C ) ) )
4 df-f 4936 . . 3  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
5 df-f 4936 . . 3  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
63, 4, 53imtr4g 203 . 2  |-  ( B 
C_  C  ->  ( F : A --> B  ->  F : A --> C ) )
76impcom 123 1  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    C_ wss 2974   ran crn 4372    Fn wfn 4927   -->wf 4928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987  df-f 4936
This theorem is referenced by:  fssd  5086  fconst6g  5116  f1ss  5128  ffoss  5189  fsn2  5369  ofco  5760  tposf2  5917  issmo2  5938  smoiso  5951  ssdomg  6325  1fv  9226  abscn2  10291  recn2  10293  imcn2  10294  climabs  10296  climre  10298  climim  10299
  Copyright terms: Public domain W3C validator