Theorem f1ocnv 5584

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 5418	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5178	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5408	. . . . . . 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 5579	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5579	. 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 1395  ^◡ccnv 4717  Rel wrel 4723   Fn wfn 5312  –1-1-onto→wf1o 5316

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-opab 4145  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-fun 5319  df-fn 5320  df-f 5321  df-f1 5322  df-fo 5323  df-f1o 5324

This theorem is referenced by:  f1ocnvb  5585  f1orescnv  5587  f1imacnv  5588  f1cnv  5595  f1ococnv1  5600  f1oresrab  5799  f1ocnvfv2  5901  f1ocnvdm  5904  f1ocnvfvrneq  5905  fcof1o  5912  isocnv  5934  f1ofveu  5988  mapsnf1o3  6842  ener  6929  en0  6945  en1  6949  en2  6971  mapen  7003  ssenen  7008  preimaf1ofi  7114  ordiso2  7198  caseinl  7254  caseinr  7255  ctssdccl  7274  ctssdclemr  7275  enomnilem  7301  enmkvlem  7324  enwomnilem  7332  cc3  7450  fnn0nninf  10655  0tonninf  10657  1tonninf  10658  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemmo  10722  iseqf1olemqk  10724  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemstep  10731  seqf1oglem1  10736  seqf1oglem2  10737  hashfz1  11000  hashfacen  11053  seq3coll  11059  cnrecnv  11416  nnf1o  11882  summodclem3  11886  summodclem2a  11887  prodmodclem3  12081  prodmodclem2a  12082  fprodssdc  12096  sqpweven  12692  2sqpwodd  12693  phimullem  12742  eulerthlemh  12748  1arith2  12886  xpnnen  12960  ennnfonelemjn  12968  ennnfonelemp1  12972  ennnfonelemhdmp1  12975  ennnfonelemss  12976  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemf1  12984  ennnfonelemnn0  12988  ennnfonelemim  12990  ctinfomlemom  12993  ctiunctlemfo  13005  ssnnctlemct  13012  mhmf1o  13498  ghmf1o  13807  gsumfzreidx  13869  znleval  14611  txhmeo  14987  dfrelog  15528  relogf1o  15529  012of  16316  domomsubct  16326  exmidsbthrlem  16349  iswomninnlem  16376