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

Theorem fss 5220
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 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)

Proof of Theorem fss
StepHypRef Expression
1 sstr2 3054 . . . . 5 (ran 𝐹𝐵 → (𝐵𝐶 → ran 𝐹𝐶))
21com12 30 . . . 4 (𝐵𝐶 → (ran 𝐹𝐵 → ran 𝐹𝐶))
32anim2d 333 . . 3 (𝐵𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶)))
4 df-f 5063 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
5 df-f 5063 . . 3 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
63, 4, 53imtr4g 204 . 2 (𝐵𝐶 → (𝐹:𝐴𝐵𝐹:𝐴𝐶))
76impcom 124 1 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wss 3021  ran crn 4478   Fn wfn 5054  wf 5055
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034  df-f 5063
This theorem is referenced by:  fssd  5221  fconst6g  5257  f1ss  5270  ffoss  5333  fsn2  5526  ofco  5931  tposf2  6095  issmo2  6116  smoiso  6129  mapsn  6514  ssdomg  6602  omp1eomlem  6894  1fv  9757  fxnn0nninf  10052  abscn2  10923  recn2  10925  imcn2  10926  climabs  10928  climre  10930  climim  10931  fsumre  11080  fsumim  11081  ismet2  12282
  Copyright terms: Public domain W3C validator