Theorem f1ocnv 5632

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 5459	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5218	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5449	. . . . . . 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 5627	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5627	. 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 4753  Rel wrel 4759   Fn wfn 5352  –1-1-onto→wf1o 5356

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 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115  df-opab 4177  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-fun 5359  df-fn 5360  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364

This theorem is referenced by:  f1ocnvb  5633  f1orescnv  5635  f1imacnv  5636  f1cnv  5643  f1ococnv1  5648  f1oresrab  5847  f1ocnvfv2  5957  f1ocnvdm  5960  f1ocnvfvrneq  5961  fcof1o  5968  isocnv  5990  f1ofveu  6046  mapsnf1o3  6945  ener  7032  en0  7048  en1  7052  en2  7078  mapen  7112  ssenen  7118  preimaf1ofi  7234  ordiso2  7339  caseinl  7395  caseinr  7396  ctssdccl  7415  ctssdclemr  7416  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  cc3  7598  fnn0nninf  10824  0tonninf  10826  1tonninf  10827  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemmo  10891  iseqf1olemqk  10893  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemstep  10900  seqf1oglem1  10905  seqf1oglem2  10906  hashfz1  11171  hashfacen  11233  seq3coll  11239  cnrecnv  11620  nnf1o  12087  summodclem3  12091  summodclem2a  12092  prodmodclem3  12286  prodmodclem2a  12287  fprodssdc  12301  sqpweven  12897  2sqpwodd  12898  phimullem  12947  eulerthlemh  12953  1arith2  13091  xpnnen  13229  ennnfonelemjn  13237  ennnfonelemp1  13241  ennnfonelemhdmp1  13244  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemf1  13253  ennnfonelemnn0  13257  ennnfonelemim  13259  ctinfomlemom  13262  ctiunctlemfo  13274  ssnnctlemct  13281  mhmf1o  13725  ghmf1o  14028  gsumfzreidx  14090  gfsumval  14102  znleval  14927  txhmeo  15310  dfrelog  15851  relogf1o  15852  012of  16893  domomsubct  16901  exmidsbthrlem  16928  iswomninnlem  16960