Theorem dff1o3 6861

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
dff1o3	⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶onto𝐵 ∧ Fun ◡𝐹))

Proof of Theorem dff1o3

Step	Hyp	Ref	Expression
1		3anan32 1113	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6860	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6572	. . 3 ⊢ (𝐹:𝐴⟶onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 636	. 2 ⊢ ((𝐹:𝐴⟶onto𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 306	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶onto𝐵 ∧ Fun ◡𝐹))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ^◡ccnv 5657  ran crn 5659  Fun wfun 6560   Fn wfn 6561  ⟶ontowfo 6564  ⟶1-1ontowf1o 6565

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-3an 1105  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  f1ofo  6862  resdif  6876  f1opw  7709  f11o  7993  1stconst  8148  2ndconst  8149  curry1  8152  curry2  8155  f1o2ndf1  8170  ssdomg  9065  dif1enlem  9213  phplem2  9258  php3  9262  f1opwfi  9383  cantnfp1lem3  9718  fpwwe2lem5  10759  canthp1lem2  10777  odf1o2  19838  dprdf1o  20299  relogf1o  26951  iseupthf1o  30860  padct  33407  ballotlemfrc  35270  poimirlem1  38807  poimirlem2  38808  poimirlem3  38809  poimirlem4  38810  poimirlem6  38812  poimirlem7  38813  poimirlem9  38815  poimirlem11  38817  poimirlem12  38818  poimirlem13  38819  poimirlem14  38820  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem23  38829  poimirlem24  38830  poimirlem25  38831  poimirlem29  38835  poimirlem31  38837  ntrneifv2  45341  permaxpow  46263  hfstructhf  46297  upgrimpthslem1  49278  upgrimspths  49281  idfth  50605  idsubc  50607