Theorem f1ocnv 5558

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 5392	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 5153	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5382	. . . . . . 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 5553	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5553	. 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 4693  Rel wrel 4699   Fn wfn 5286  –1-1-onto→wf1o 5290

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 4179  ax-pow 4235  ax-pr 4270

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 2779  df-un 3179  df-in 3181  df-ss 3188  df-pw 3629  df-sn 3650  df-pr 3651  df-op 3653  df-br 4061  df-opab 4123  df-xp 4700  df-rel 4701  df-cnv 4702  df-co 4703  df-dm 4704  df-rn 4705  df-fun 5293  df-fn 5294  df-f 5295  df-f1 5296  df-fo 5297  df-f1o 5298

This theorem is referenced by:  f1ocnvb  5559  f1orescnv  5561  f1imacnv  5562  f1cnv  5569  f1ococnv1  5574  f1oresrab  5770  f1ocnvfv2  5872  f1ocnvdm  5875  f1ocnvfvrneq  5876  fcof1o  5883  isocnv  5905  f1ofveu  5957  mapsnf1o3  6809  ener  6896  en0  6912  en1  6916  en2  6938  mapen  6970  ssenen  6975  preimaf1ofi  7081  ordiso2  7165  caseinl  7221  caseinr  7222  ctssdccl  7241  ctssdclemr  7242  enomnilem  7268  enmkvlem  7291  enwomnilem  7299  cc3  7417  fnn0nninf  10622  0tonninf  10624  1tonninf  10625  iseqf1olemkle  10681  iseqf1olemklt  10682  iseqf1olemqcl  10683  iseqf1olemnab  10685  iseqf1olemmo  10689  iseqf1olemqk  10691  seq3f1olemqsumkj  10695  seq3f1olemqsumk  10696  seq3f1olemstep  10698  seqf1oglem1  10703  seqf1oglem2  10704  hashfz1  10967  hashfacen  11020  seq3coll  11026  cnrecnv  11382  nnf1o  11848  summodclem3  11852  summodclem2a  11853  prodmodclem3  12047  prodmodclem2a  12048  fprodssdc  12062  sqpweven  12658  2sqpwodd  12659  phimullem  12708  eulerthlemh  12714  1arith2  12852  xpnnen  12926  ennnfonelemjn  12934  ennnfonelemp1  12938  ennnfonelemhdmp1  12941  ennnfonelemss  12942  ennnfonelemkh  12944  ennnfonelemhf1o  12945  ennnfonelemex  12946  ennnfonelemf1  12950  ennnfonelemnn0  12954  ennnfonelemim  12956  ctinfomlemom  12959  ctiunctlemfo  12971  ssnnctlemct  12978  mhmf1o  13463  ghmf1o  13772  gsumfzreidx  13834  znleval  14576  txhmeo  14952  dfrelog  15493  relogf1o  15494  012of  16238  domomsubct  16248  exmidsbthrlem  16271  iswomninnlem  16298