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

Theorem fof 5246
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
fof (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)

Proof of Theorem fof
StepHypRef Expression
1 eqimss 3079 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 335 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 5034 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 5032 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 200 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1290  wss 3000  ran crn 4453   Fn wfn 5023  wf 5024  ontowfo 5026
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 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3006  df-ss 3013  df-f 5032  df-fo 5034
This theorem is referenced by:  fofun  5247  fofn  5248  dffo2  5250  foima  5251  resdif  5288  ffoss  5298  fconstfvm  5529  cocan2  5581  foeqcnvco  5583  fornex  5900  algrflem  6008  algrflemg  6009  tposf2  6047  mapsn  6461  ssdomg  6549  fopwdom  6606  fidcenumlemrks  6716  fidcenumlemr  6718  ctmlemr  6844  ctm  6845  enumctlemm  6846  enumct  6847  fodjuomnilemdc  6860  exmidfodomrlemr  6889  exmidfodomrlemrALT  6890  focdmex  10256
  Copyright terms: Public domain W3C validator