Theorem dff1o5 6777

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 6493	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2		dffo2 6744	. . . 4 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵))
3		f1f 6724	. . . . 5 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
4	3	biantrurd 532	. . . 4 ⊢ (𝐹:𝐴–1-1→𝐵 → (ran 𝐹 = 𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)))
5	2, 4	bitr4id 290	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴–onto→𝐵 ↔ ran 𝐹 = 𝐵))
6	5	pm5.32i 574	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵) ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))
7	1, 6	bitri 275	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ ran 𝐹 = 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ran crn 5624  ⟶wf 6482  –1-1→wf1 6483  –onto→wfo 6484  –1-1-onto→wf1o 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  f1orescnv  6783  f1ounsn  7213  domdifsn  8984  sucdom2  9127  ackbij1  10150  ackbij2  10155  fin4en1  10222  om2uzf1oi  13879  s4f1o  14844  fvcosymgeq  19327  indlcim  21766  2lgslem1b  27320  ausgrusgrb  29129  usgrexmpledg  29226  wrdpmtrlast  33054  onvf1od  35099  cdleme50f1o  40545  diaf1oN  41129  aks6d1c2  42123  pwssplit4  43082  cantnf2  43318  meadjiunlem  46466