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

Theorem f1ss 5302
Description: A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Mario Carneiro, 12-Jan-2013.)
Assertion
Ref Expression
f1ss ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)

Proof of Theorem f1ss
StepHypRef Expression
1 f1f 5296 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 5252 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 279 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 5096 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 271 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 272 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 5096 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 411 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wss 3039  ccnv 4506  Fun wfun 5085  wf 5087  1-1wf1 5088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052  df-f 5095  df-f1 5096
This theorem is referenced by:  f1sng  5375
  Copyright terms: Public domain W3C validator