Theorem dffo2 6751

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 6747	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		forn 6750	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
3	1, 2	jca 511	. 2 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
4		ffn 6663	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
5		df-fo 6499	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
6	5	biimpri 228	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵)
7	4, 6	sylan 581	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴–onto→𝐵)
8	3, 7	impbii 209	1 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ran crn 5626   Fn wfn 6488  ⟶wf 6489  –onto→wfo 6491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3919  df-f 6497  df-fo 6499

This theorem is referenced by:  focofo  6760  foconst  6762  dff1o5  6784  dffo3  7049  dffo4  7050  exfo  7052  dffo3f  7053  fo1stres  7962  fo2ndres  7963  fo2ndf  8066  cantnf  9607  hsmexlem2  10342  setcepi  18017  odf1o1  19506  efgsfo  19673  pjfo  21675  xrhmeo  24905  grpofo  30579  cnpconn  35437  lnmepi  43405  imasetpreimafvbijlemfo  47728  fargshiftfo  47765