Theorem dffo2 6767

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 6763	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		forn 6766	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
3	1, 2	jca 518	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
4		ffn 6676	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
5		df-fo 6512	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
6	5	biimpri 230	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵)
7	4, 6	sylan 588	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵)
8	3, 7	impbii 211	1 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1550  ran crn 5637   Fn wfn 6501  ⟶wf 6502  –onto→wfo 6504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-ss 3912  df-f 6510  df-fo 6512

This theorem is referenced by:  focofo  6776  foconst  6778  dff1o5  6801  dffo3  7068  dffo4  7069  exfo  7071  dffo3f  7072  fo1stres  7981  fo2ndres  7982  fo2ndf  8084  cantnf  9634  hsmexlem2  10370  setcepi  18093  odf1o1  19584  efgsfo  19751  pjfo  21736  xrhmeo  24977  grpofo  30637  cnpconn  35518  lnmepi  43600  imasetpreimafvbijlemfo  47949  fargshiftfo  47986