Theorem f1ocnv 5605

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 5435	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5194	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5425	. . . . . . 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 5600	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5600	. 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 4730  Rel wrel 4736   Fn wfn 5328  –1-1-onto→wf1o 5332

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-opab 4156  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-fun 5335  df-fn 5336  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340

This theorem is referenced by:  f1ocnvb  5606  f1orescnv  5608  f1imacnv  5609  f1cnv  5616  f1ococnv1  5621  f1oresrab  5820  f1ocnvfv2  5929  f1ocnvdm  5932  f1ocnvfvrneq  5933  fcof1o  5940  isocnv  5962  f1ofveu  6016  mapsnf1o3  6909  ener  6996  en0  7012  en1  7016  en2  7041  mapen  7075  ssenen  7080  preimaf1ofi  7193  ordiso2  7277  caseinl  7333  caseinr  7334  ctssdccl  7353  ctssdclemr  7354  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  cc3  7530  fnn0nninf  10746  0tonninf  10748  1tonninf  10749  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemmo  10813  iseqf1olemqk  10815  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemstep  10822  seqf1oglem1  10827  seqf1oglem2  10828  hashfz1  11091  hashfacen  11146  seq3coll  11152  cnrecnv  11533  nnf1o  12000  summodclem3  12004  summodclem2a  12005  prodmodclem3  12199  prodmodclem2a  12200  fprodssdc  12214  sqpweven  12810  2sqpwodd  12811  phimullem  12860  eulerthlemh  12866  1arith2  13004  xpnnen  13078  ennnfonelemjn  13086  ennnfonelemp1  13090  ennnfonelemhdmp1  13093  ennnfonelemss  13094  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemf1  13102  ennnfonelemnn0  13106  ennnfonelemim  13108  ctinfomlemom  13111  ctiunctlemfo  13123  ssnnctlemct  13130  mhmf1o  13616  ghmf1o  13925  gsumfzreidx  13987  znleval  14732  txhmeo  15113  dfrelog  15654  relogf1o  15655  012of  16696  domomsubct  16706  exmidsbthrlem  16733  iswomninnlem  16765  gfsumval  16792