Theorem f1f1orn 5653

Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)

Assertion

Ref	Expression
f1f1orn	⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

Proof of Theorem f1f1orn

Step	Hyp	Ref	Expression
1		f1fn 5603	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		df-f1 5385	. . 3 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 275	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → Fun ◡𝐹)
4		f1orn 5652	. 2 ⊢ (𝐹:𝐴–1-1-onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹))
5	1, 3, 4	sylanbrc 421	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran 𝐹)

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 4775  ran crn 4777  Fun wfun 5374   Fn wfn 5375  ⟶wf 5376  –1-1→wf1 5377  –1-1-onto→wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387

This theorem is used by:  f1ores  5657  f1cnv  5666  f1cocnv1  5672  f1ocnvfvrneq  5991  ssenen  7156  f1dmvrnfibi  7262  cc2lem  7638  hashf1lem1  11307  hashf1lem2  11308  4sqlem11  13209  xpsff1o2  13731  imasmndf1  13820  imasgrpf1  13974  conjsubgen  14140  imasrngf1  14363  imasringf1  14479  usgrf1o  16620  uspgrf1oedg  16622