Theorem f1ocnv 5266

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 5112	. . . . 5 |- ( F Fn A -> Rel F )
2		dfrel2 4881	. . . . . 6 |- ( Rel F <-> `' `' F = F )
3		fneq1 5102	. . . . . . 7 |- ( `' `' F = F -> ( `' `' F Fn A <-> F Fn A ) )
4	3	biimprd 156	. . . . . 6 |- ( `' `' F = F -> ( F Fn A -> `' `' F Fn A ) )
5	2, 4	sylbi 119	. . . . 5 |- ( Rel F -> ( F Fn A -> `' `' F Fn A ) )
6	1, 5	mpcom 36	. . . 4 |- ( F Fn A -> `' `' F Fn A )
7	6	anim2i 334	. . 3 |- ( ( `' F Fn B /\ F Fn A ) -> ( `' F Fn B /\ `' `' F Fn A ) )
8	7	ancoms 264	. 2 |- ( ( F Fn A /\ `' F Fn B ) -> ( `' F Fn B /\ `' `' F Fn A ) )
9		dff1o4 5261	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
10		dff1o4 5261	. 2 |- ( `' F : B -1-1-onto-> A <-> ( `' F Fn B /\ `' `' F Fn A ) )
11	8, 9, 10	3imtr4i 199	1 |- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1289   `'ccnv 4437   Rel wrel 4443   Fn wfn 5010   -1-1-onto->wf1o 5014

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-br 3846  df-opab 3900  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022

This theorem is referenced by:  f1ocnvb  5267  f1orescnv  5269  f1imacnv  5270  f1cnv  5277  f1ococnv1  5282  f1oresrab  5463  f1ocnvfv2  5557  f1ocnvdm  5560  f1ocnvfvrneq  5561  fcof1o  5568  isocnv  5590  f1ofveu  5640  mapsnf1o3  6454  ener  6496  en0  6512  en1  6516  mapen  6562  ssenen  6567  preimaf1ofi  6660  ordiso2  6728  enomnilem  6794  fnn0nninf  9843  0tonninf  9845  1tonninf  9846  iseqf1olemkle  9913  iseqf1olemklt  9914  iseqf1olemqcl  9915  iseqf1olemnab  9917  iseqf1olemmo  9921  iseqf1olemqk  9923  seq3f1olemqsumkj  9927  seq3f1olemqsumk  9928  seq3f1olemstep  9930  hashfz1  10191  hashfacen  10241  iseqcoll  10247  cnrecnv  10344  isummolemnm  10769  isummolem3  10770  isummolem2a  10771  sqpweven  11431  2sqpwodd  11432  phimullem  11479  xpnnen  11485  exmidsbthrlem  11912