Theorem f1ocnv 5453

Description: The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
f1ocnv	|- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )

Proof of Theorem f1ocnv

Step	Hyp	Ref	Expression
1		fnrel 5294	. . . . 5 |- ( F Fn A -> Rel F )
2		dfrel2 5059	. . . . . 6 |- ( Rel F <-> `' `' F = F )
3		fneq1 5284	. . . . . . 7 |- ( `' `' F = F -> ( `' `' F Fn A <-> F Fn A ) )
4	3	biimprd 157	. . . . . 6 |- ( `' `' F = F -> ( F Fn A -> `' `' F Fn A ) )
5	2, 4	sylbi 120	. . . . 5 |- ( Rel F -> ( F Fn A -> `' `' F Fn A ) )
6	1, 5	mpcom 36	. . . 4 |- ( F Fn A -> `' `' F Fn A )
7	6	anim2i 340	. . 3 |- ( ( `' F Fn B /\ F Fn A ) -> ( `' F Fn B /\ `' `' F Fn A ) )
8	7	ancoms 266	. 2 |- ( ( F Fn A /\ `' F Fn B ) -> ( `' F Fn B /\ `' `' F Fn A ) )
9		dff1o4 5448	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
10		dff1o4 5448	. 2 |- ( `' F : B -1-1-onto-> A <-> ( `' F Fn B /\ `' `' F Fn A ) )
11	8, 9, 10	3imtr4i 200	1 |- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348   `'ccnv 4608   Rel wrel 4614   Fn wfn 5191   -1-1-onto->wf1o 5195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988  df-opab 4049  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203

This theorem is referenced by:  f1ocnvb  5454  f1orescnv  5456  f1imacnv  5457  f1cnv  5464  f1ococnv1  5469  f1oresrab  5658  f1ocnvfv2  5754  f1ocnvdm  5757  f1ocnvfvrneq  5758  fcof1o  5765  isocnv  5787  f1ofveu  5838  mapsnf1o3  6671  ener  6753  en0  6769  en1  6773  mapen  6820  ssenen  6825  preimaf1ofi  6924  ordiso2  7008  caseinl  7064  caseinr  7065  ctssdccl  7084  ctssdclemr  7085  enomnilem  7110  enmkvlem  7133  enwomnilem  7141  cc3  7217  fnn0nninf  10380  0tonninf  10382  1tonninf  10383  iseqf1olemkle  10427  iseqf1olemklt  10428  iseqf1olemqcl  10429  iseqf1olemnab  10431  iseqf1olemmo  10435  iseqf1olemqk  10437  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3f1olemstep  10444  hashfz1  10704  hashfacen  10758  seq3coll  10764  cnrecnv  10861  nnf1o  11326  summodclem3  11330  summodclem2a  11331  prodmodclem3  11525  prodmodclem2a  11526  fprodssdc  11540  sqpweven  12116  2sqpwodd  12117  phimullem  12166  eulerthlemh  12172  1arith2  12307  xpnnen  12336  ennnfonelemjn  12344  ennnfonelemp1  12348  ennnfonelemhdmp1  12351  ennnfonelemss  12352  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemf1  12360  ennnfonelemnn0  12364  ennnfonelemim  12366  ctinfomlemom  12369  ctiunctlemfo  12381  ssnnctlemct  12388  mhmf1o  12680  txhmeo  13072  dfrelog  13534  relogf1o  13535  012of  13988  exmidsbthrlem  14014  iswomninnlem  14041