Theorem dffo2 6822

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 6818	. . 3 ⊢ (𝐹:𝐴⟶onto𝐵 → 𝐹:𝐴⟶𝐵)
2		forn 6821	. . 3 ⊢ (𝐹:𝐴⟶onto𝐵 → ran 𝐹 = 𝐵)
3	1, 2	jca 521	. 2 ⊢ (𝐹:𝐴⟶onto𝐵 → (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
4		ffn 6731	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
5		df-fo 6564	. . . 4 ⊢ (𝐹:𝐴⟶onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
6	5	biimpri 231	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶onto𝐵)
7	4, 6	sylan 592	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶onto𝐵)
8	3, 7	impbii 212	1 ⊢ (𝐹:𝐴⟶onto𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ran crn 5656   Fn wfn 6553  ⟶wf 6554  ⟶ontowfo 6556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6562  df-fo 6564

This theorem is used by:  focofo  6831  foconst  6833  dff1o5  6856  dffo3  7126  dffo4  7127  exfo  7129  dffo3f  7130  fo1stres  8051  fo2ndres  8052  fo2ndf  8159  cantnf  9721  hsmexlem2  10532  setcepi  18292  odf1o1  19816  efgsfo  19983  pjfo  22051  xrhmeo  25297  grpofo  31131  cnpconn  36162  lnmepi  44280  imasetpreimafvbijlemfo  48692  fargshiftfo  48729