Theorem dff1o5 6864

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

Assertion

Ref	Expression
dff1o5	⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dff1o5

Step	Hyp	Ref	Expression
1		df-f1o 6573	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶1-1𝐵 ∧ 𝐹:𝐴⟶onto𝐵))
2		dffo2 6830	. . . 4 ⊢ (𝐹:𝐴⟶onto𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
3		f1f 6808	. . . . 5 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹:𝐴⟶𝐵)
4	3	biantrurd 542	. . . 4 ⊢ (𝐹:𝐴⟶1-1𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)))
5	2, 4	bitr4id 293	. . 3 ⊢ (𝐹:𝐴⟶1-1𝐵 → (𝐹:𝐴⟶onto𝐵 ↔ ran 𝐹 = 𝐵))
6	5	pm5.32i 585	. 2 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐹:𝐴⟶onto𝐵) ↔ (𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 = 𝐵))
7	1, 6	bitri 278	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶1-1𝐵 ∧ ran 𝐹 = 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ran crn 5659  ⟶wf 6562  ⟶1-1wf1 6563  ⟶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-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:  f1orescnv  6870  f1ounsn  7311  domdifsn  9117  sucdom2  9256  ackbij1  10354  ackbij2  10359  fin4en1  10426  om2uzf1oi  14136  s4f1o  15112  fvcosymgeq  19694  indlcim  22201  2lgslem1b  27776  ausgrusgrb  29803  usgrexmpledg  29900  wrdpmtrlast  33753  jf1o  36052  onvf1od  36076  onprcf1of1ord  36096  cdleme50f1o  41869  diaf1oN  42453  aks6d1c2  43446  pwssplit4  44357  cantnf2  44588  hfstructcan  46298  meadjiunlem  47748