Theorem f1ocnv 5596

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 5428	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5187	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5418	. . . . . . 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 5591	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5591	. 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 1397  ^◡ccnv 4724  Rel wrel 4730   Fn wfn 5321  –1-1-onto→wf1o 5325

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333

This theorem is referenced by:  f1ocnvb  5597  f1orescnv  5599  f1imacnv  5600  f1cnv  5607  f1ococnv1  5612  f1oresrab  5812  f1ocnvfv2  5919  f1ocnvdm  5922  f1ocnvfvrneq  5923  fcof1o  5930  isocnv  5952  f1ofveu  6006  mapsnf1o3  6866  ener  6953  en0  6969  en1  6973  en2  6998  mapen  7032  ssenen  7037  preimaf1ofi  7150  ordiso2  7234  caseinl  7290  caseinr  7291  ctssdccl  7310  ctssdclemr  7311  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  cc3  7487  fnn0nninf  10701  0tonninf  10703  1tonninf  10704  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemmo  10768  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemstep  10777  seqf1oglem1  10782  seqf1oglem2  10783  hashfz1  11046  hashfacen  11101  seq3coll  11107  cnrecnv  11475  nnf1o  11942  summodclem3  11946  summodclem2a  11947  prodmodclem3  12141  prodmodclem2a  12142  fprodssdc  12156  sqpweven  12752  2sqpwodd  12753  phimullem  12802  eulerthlemh  12808  1arith2  12946  xpnnen  13020  ennnfonelemjn  13028  ennnfonelemp1  13032  ennnfonelemhdmp1  13035  ennnfonelemss  13036  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemex  13040  ennnfonelemf1  13044  ennnfonelemnn0  13048  ennnfonelemim  13050  ctinfomlemom  13053  ctiunctlemfo  13065  ssnnctlemct  13072  mhmf1o  13558  ghmf1o  13867  gsumfzreidx  13929  znleval  14673  txhmeo  15049  dfrelog  15590  relogf1o  15591  012of  16618  domomsubct  16628  exmidsbthrlem  16652  iswomninnlem  16680  gfsumval  16707