Theorem dff1o5 6611

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-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dff1o5

Step	Hyp	Ref	Expression
1		df-f1o 6342	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		dffo2 6580	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
3		f1f 6560	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
4	3	biantrurd 536	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)))
5	2, 4	bitr4id 293	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴–onto→𝐵 ↔ ran 𝐹 = 𝐵))
6	5	pm5.32i 578	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))
7	1, 6	bitri 278	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ran crn 5525  ⟶wf 6331  –1-1→wf1 6332  –onto→wfo 6333  –1-1-onto→wf1o 6334

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342

This theorem is referenced by:  f1orescnv  6617  domdifsn  8621  sucdom2  8648  ackbij1  9698  ackbij2  9703  fin4en1  9769  om2uzf1oi  13370  s4f1o  14327  fvcosymgeq  18624  indlcim  20605  2lgslem1b  26075  ausgrusgrb  27057  usgrexmpledg  27151  cdleme50f1o  38122  diaf1oN  38706  pwssplit4  40406  meadjiunlem  43470