Theorem dffo2 6692

Description: Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)

Assertion

Ref	Expression
dffo2	⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dffo2

Step	Hyp	Ref	Expression
1		fof 6688	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		forn 6691	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
3	1, 2	jca 512	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
4		ffn 6600	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
5		df-fo 6439	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
6	5	biimpri 227	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵)
7	4, 6	sylan 580	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵)
8	3, 7	impbii 208	1 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ran crn 5590   Fn wfn 6428  ⟶wf 6429  –onto→wfo 6431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437  df-fo 6439

This theorem is referenced by:  focofo  6701  foconst  6703  dff1o5  6725  dffo3  6978  dffo4  6979  exfo  6981  fo1stres  7857  fo2ndres  7858  fo2ndf  7962  cantnf  9451  hsmexlem2  10183  setcepi  17803  odf1o1  19177  efgsfo  19345  pjfo  20922  xrhmeo  24109  grpofo  28861  cnpconn  33192  lnmepi  40910  dffo3f  42717  imasetpreimafvbijlemfo  44857  fargshiftfo  44894