Theorem f1ocnv 5627

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 5454	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5213	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5444	. . . . . . 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 5622	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5622	. 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 1398  ^◡ccnv 4748  Rel wrel 4754   Fn wfn 5347  –1-1-onto→wf1o 5351

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 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110  df-opab 4172  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359

This theorem is referenced by:  f1ocnvb  5628  f1orescnv  5630  f1imacnv  5631  f1cnv  5638  f1ococnv1  5643  f1oresrab  5842  f1ocnvfv2  5951  f1ocnvdm  5954  f1ocnvfvrneq  5955  fcof1o  5962  isocnv  5984  f1ofveu  6038  mapsnf1o3  6932  ener  7019  en0  7035  en1  7039  en2  7065  mapen  7099  ssenen  7105  preimaf1ofi  7221  ordiso2  7326  caseinl  7382  caseinr  7383  ctssdccl  7402  ctssdclemr  7403  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  cc3  7582  fnn0nninf  10800  0tonninf  10802  1tonninf  10803  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemmo  10867  iseqf1olemqk  10869  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemstep  10876  seqf1oglem1  10881  seqf1oglem2  10882  hashfz1  11146  hashfacen  11208  seq3coll  11214  cnrecnv  11595  nnf1o  12062  summodclem3  12066  summodclem2a  12067  prodmodclem3  12261  prodmodclem2a  12262  fprodssdc  12276  sqpweven  12872  2sqpwodd  12873  phimullem  12922  eulerthlemh  12928  1arith2  13066  xpnnen  13145  ennnfonelemjn  13153  ennnfonelemp1  13157  ennnfonelemhdmp1  13160  ennnfonelemss  13161  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemf1  13169  ennnfonelemnn0  13173  ennnfonelemim  13175  ctinfomlemom  13178  ctiunctlemfo  13190  ssnnctlemct  13197  mhmf1o  13683  ghmf1o  13992  gsumfzreidx  14054  znleval  14801  txhmeo  15184  dfrelog  15725  relogf1o  15726  012of  16767  domomsubct  16775  exmidsbthrlem  16802  iswomninnlem  16834  gfsumval  16862