Theorem f1ocnv 5629

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 5456	. . . . 5 |- ( F Fn A -> Rel F )
2		dfrel2 5215	. . . . . 6 |- ( Rel F <-> `' `' F = F )
3		fneq1 5446	. . . . . . 7 |- ( `' `' F = F -> ( `' `' F Fn A <-> F Fn A ) )
4	3	biimprd 158	. . . . . 6 |- ( `' `' F = F -> ( F Fn A -> `' `' F Fn A ) )
5	2, 4	sylbi 121	. . . . 5 |- ( Rel F -> ( F Fn A -> `' `' F Fn A ) )
6	1, 5	mpcom 36	. . . 4 |- ( F Fn A -> `' `' F Fn A )
7	6	anim2i 342	. . 3 |- ( ( `' F Fn B /\ F Fn A ) -> ( `' F Fn B /\ `' `' F Fn A ) )
8	7	ancoms 268	. 2 |- ( ( F Fn A /\ `' F Fn B ) -> ( `' F Fn B /\ `' `' F Fn A ) )
9		dff1o4 5624	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
10		dff1o4 5624	. 2 |- ( `' F : B -1-1-onto-> A <-> ( `' F Fn B /\ `' `' F Fn A ) )
11	8, 9, 10	3imtr4i 201	1 |- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   `'ccnv 4750   Rel wrel 4756   Fn wfn 5349   -1-1-onto->wf1o 5353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112  df-opab 4174  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-fun 5356  df-fn 5357  df-f 5358  df-f1 5359  df-fo 5360  df-f1o 5361

This theorem is referenced by:  f1ocnvb  5630  f1orescnv  5632  f1imacnv  5633  f1cnv  5640  f1ococnv1  5645  f1oresrab  5844  f1ocnvfv2  5953  f1ocnvdm  5956  f1ocnvfvrneq  5957  fcof1o  5964  isocnv  5986  f1ofveu  6040  mapsnf1o3  6934  ener  7021  en0  7037  en1  7041  en2  7067  mapen  7101  ssenen  7107  preimaf1ofi  7223  ordiso2  7328  caseinl  7384  caseinr  7385  ctssdccl  7404  ctssdclemr  7405  enomnilem  7431  enmkvlem  7454  enwomnilem  7462  cc3  7584  fnn0nninf  10804  0tonninf  10806  1tonninf  10807  iseqf1olemkle  10863  iseqf1olemklt  10864  iseqf1olemqcl  10865  iseqf1olemnab  10867  iseqf1olemmo  10871  iseqf1olemqk  10873  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seq3f1olemstep  10880  seqf1oglem1  10885  seqf1oglem2  10886  hashfz1  11150  hashfacen  11212  seq3coll  11218  cnrecnv  11599  nnf1o  12066  summodclem3  12070  summodclem2a  12071  prodmodclem3  12265  prodmodclem2a  12266  fprodssdc  12280  sqpweven  12876  2sqpwodd  12877  phimullem  12926  eulerthlemh  12932  1arith2  13070  xpnnen  13162  ennnfonelemjn  13170  ennnfonelemp1  13174  ennnfonelemhdmp1  13177  ennnfonelemss  13178  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ennnfonelemex  13182  ennnfonelemf1  13186  ennnfonelemnn0  13190  ennnfonelemim  13192  ctinfomlemom  13195  ctiunctlemfo  13207  ssnnctlemct  13214  mhmf1o  13700  ghmf1o  14009  gsumfzreidx  14071  znleval  14818  txhmeo  15201  dfrelog  15742  relogf1o  15743  012of  16784  domomsubct  16792  exmidsbthrlem  16819  iswomninnlem  16851  gfsumval  16879