Theorem f1ocnv 5557

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 5391	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5152	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5381	. . . . . . 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 5552	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5552	. 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 1373  ^◡ccnv 4692  Rel wrel 4698   Fn wfn 5285  –1-1-onto→wf1o 5289

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060  df-opab 4122  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-fun 5292  df-fn 5293  df-f 5294  df-f1 5295  df-fo 5296  df-f1o 5297

This theorem is referenced by:  f1ocnvb  5558  f1orescnv  5560  f1imacnv  5561  f1cnv  5568  f1ococnv1  5573  f1oresrab  5768  f1ocnvfv2  5870  f1ocnvdm  5873  f1ocnvfvrneq  5874  fcof1o  5881  isocnv  5903  f1ofveu  5955  mapsnf1o3  6807  ener  6894  en0  6910  en1  6914  en2  6936  mapen  6968  ssenen  6973  preimaf1ofi  7079  ordiso2  7163  caseinl  7219  caseinr  7220  ctssdccl  7239  ctssdclemr  7240  enomnilem  7266  enmkvlem  7289  enwomnilem  7297  cc3  7415  fnn0nninf  10620  0tonninf  10622  1tonninf  10623  iseqf1olemkle  10679  iseqf1olemklt  10680  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemmo  10687  iseqf1olemqk  10689  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemstep  10696  seqf1oglem1  10701  seqf1oglem2  10702  hashfz1  10965  hashfacen  11018  seq3coll  11024  cnrecnv  11336  nnf1o  11802  summodclem3  11806  summodclem2a  11807  prodmodclem3  12001  prodmodclem2a  12002  fprodssdc  12016  sqpweven  12612  2sqpwodd  12613  phimullem  12662  eulerthlemh  12668  1arith2  12806  xpnnen  12880  ennnfonelemjn  12888  ennnfonelemp1  12892  ennnfonelemhdmp1  12895  ennnfonelemss  12896  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemf1  12904  ennnfonelemnn0  12908  ennnfonelemim  12910  ctinfomlemom  12913  ctiunctlemfo  12925  ssnnctlemct  12932  mhmf1o  13417  ghmf1o  13726  gsumfzreidx  13788  znleval  14530  txhmeo  14906  dfrelog  15447  relogf1o  15448  012of  16130  domomsubct  16140  exmidsbthrlem  16163  iswomninnlem  16190