Theorem f1ocnv 5535

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 5372	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5133	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5362	. . . . . . 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 5530	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5530	. 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 4674  Rel wrel 4680   Fn wfn 5266  –1-1-onto→wf1o 5270

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045  df-opab 4106  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278

This theorem is referenced by:  f1ocnvb  5536  f1orescnv  5538  f1imacnv  5539  f1cnv  5546  f1ococnv1  5551  f1oresrab  5745  f1ocnvfv2  5847  f1ocnvdm  5850  f1ocnvfvrneq  5851  fcof1o  5858  isocnv  5880  f1ofveu  5932  mapsnf1o3  6784  ener  6871  en0  6887  en1  6891  en2  6912  mapen  6943  ssenen  6948  preimaf1ofi  7053  ordiso2  7137  caseinl  7193  caseinr  7194  ctssdccl  7213  ctssdclemr  7214  enomnilem  7240  enmkvlem  7263  enwomnilem  7271  cc3  7380  fnn0nninf  10583  0tonninf  10585  1tonninf  10586  iseqf1olemkle  10642  iseqf1olemklt  10643  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemmo  10650  iseqf1olemqk  10652  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemstep  10659  seqf1oglem1  10664  seqf1oglem2  10665  hashfz1  10928  hashfacen  10981  seq3coll  10987  cnrecnv  11221  nnf1o  11687  summodclem3  11691  summodclem2a  11692  prodmodclem3  11886  prodmodclem2a  11887  fprodssdc  11901  sqpweven  12497  2sqpwodd  12498  phimullem  12547  eulerthlemh  12553  1arith2  12691  xpnnen  12765  ennnfonelemjn  12773  ennnfonelemp1  12777  ennnfonelemhdmp1  12780  ennnfonelemss  12781  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemf1  12789  ennnfonelemnn0  12793  ennnfonelemim  12795  ctinfomlemom  12798  ctiunctlemfo  12810  ssnnctlemct  12817  mhmf1o  13302  ghmf1o  13611  gsumfzreidx  13673  znleval  14415  txhmeo  14791  dfrelog  15332  relogf1o  15333  012of  15930  domomsubct  15938  exmidsbthrlem  15961  iswomninnlem  15988