Theorem f1ocnv 5444

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 5285	. . . . 5 |- ( F Fn A -> Rel F )
2		dfrel2 5053	. . . . . 6 |- ( Rel F <-> `' `' F = F )
3		fneq1 5275	. . . . . . 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 5439	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
10		dff1o4 5439	. 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 1343   `'ccnv 4602   Rel wrel 4608   Fn wfn 5182   -1-1-onto->wf1o 5186

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-pow 4152  ax-pr 4186

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-pw 3560  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982  df-opab 4043  df-xp 4609  df-rel 4610  df-cnv 4611  df-co 4612  df-dm 4613  df-rn 4614  df-fun 5189  df-fn 5190  df-f 5191  df-f1 5192  df-fo 5193  df-f1o 5194

This theorem is referenced by:  f1ocnvb  5445  f1orescnv  5447  f1imacnv  5448  f1cnv  5455  f1ococnv1  5460  f1oresrab  5649  f1ocnvfv2  5745  f1ocnvdm  5748  f1ocnvfvrneq  5749  fcof1o  5756  isocnv  5778  f1ofveu  5829  mapsnf1o3  6659  ener  6741  en0  6757  en1  6761  mapen  6808  ssenen  6813  preimaf1ofi  6912  ordiso2  6996  caseinl  7052  caseinr  7053  ctssdccl  7072  ctssdclemr  7073  enomnilem  7098  enmkvlem  7121  enwomnilem  7129  cc3  7205  fnn0nninf  10368  0tonninf  10370  1tonninf  10371  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemmo  10423  iseqf1olemqk  10425  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemstep  10432  hashfz1  10692  hashfacen  10745  seq3coll  10751  cnrecnv  10848  nnf1o  11313  summodclem3  11317  summodclem2a  11318  prodmodclem3  11512  prodmodclem2a  11513  fprodssdc  11527  sqpweven  12103  2sqpwodd  12104  phimullem  12153  eulerthlemh  12159  1arith2  12294  xpnnen  12323  ennnfonelemjn  12331  ennnfonelemp1  12335  ennnfonelemhdmp1  12338  ennnfonelemss  12339  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemf1  12347  ennnfonelemnn0  12351  ennnfonelemim  12353  ctinfomlemom  12356  ctiunctlemfo  12368  ssnnctlemct  12375  txhmeo  12919  dfrelog  13381  relogf1o  13382  012of  13835  exmidsbthrlem  13861  iswomninnlem  13888