Theorem f1ocnv 5534

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	⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Proof of Theorem f1ocnv

Step	Hyp	Ref	Expression
1		fnrel 5371	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5132	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5361	. . . . . . 7 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 158	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 121	. . . . 5 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 36	. . . 4 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim2i 342	. . 3 ⊢ ((◡𝐹 Fn 𝐵 ∧ 𝐹 Fn 𝐴) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8	7	ancoms 268	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
9		dff1o4 5529	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5529	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
11	8, 9, 10	3imtr4i 201	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1372  ^◡ccnv 4673  Rel wrel 4679   Fn wfn 5265  –1-1-onto→wf1o 5269

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044  df-opab 4105  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-fun 5272  df-fn 5273  df-f 5274  df-f1 5275  df-fo 5276  df-f1o 5277

This theorem is referenced by:  f1ocnvb  5535  f1orescnv  5537  f1imacnv  5538  f1cnv  5545  f1ococnv1  5550  f1oresrab  5744  f1ocnvfv2  5846  f1ocnvdm  5849  f1ocnvfvrneq  5850  fcof1o  5857  isocnv  5879  f1ofveu  5931  mapsnf1o3  6783  ener  6870  en0  6886  en1  6890  en2  6911  mapen  6942  ssenen  6947  preimaf1ofi  7052  ordiso2  7136  caseinl  7192  caseinr  7193  ctssdccl  7212  ctssdclemr  7213  enomnilem  7239  enmkvlem  7262  enwomnilem  7270  cc3  7379  fnn0nninf  10581  0tonninf  10583  1tonninf  10584  iseqf1olemkle  10640  iseqf1olemklt  10641  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemmo  10648  iseqf1olemqk  10650  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemstep  10657  seqf1oglem1  10662  seqf1oglem2  10663  hashfz1  10926  hashfacen  10979  seq3coll  10985  cnrecnv  11192  nnf1o  11658  summodclem3  11662  summodclem2a  11663  prodmodclem3  11857  prodmodclem2a  11858  fprodssdc  11872  sqpweven  12468  2sqpwodd  12469  phimullem  12518  eulerthlemh  12524  1arith2  12662  xpnnen  12736  ennnfonelemjn  12744  ennnfonelemp1  12748  ennnfonelemhdmp1  12751  ennnfonelemss  12752  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ennnfonelemex  12756  ennnfonelemf1  12760  ennnfonelemnn0  12764  ennnfonelemim  12766  ctinfomlemom  12769  ctiunctlemfo  12781  ssnnctlemct  12788  mhmf1o  13273  ghmf1o  13582  gsumfzreidx  13644  znleval  14386  txhmeo  14762  dfrelog  15303  relogf1o  15304  012of  15892  domomsubct  15900  exmidsbthrlem  15923  iswomninnlem  15950