Theorem f1ocnv 5301

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 5146	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 4915	. . . . . 6 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 5136	. . . . . . 7 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 157	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 120	. . . . 5 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 36	. . . 4 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim2i 335	. . 3 ⊢ ((◡𝐹 Fn 𝐵 ∧ 𝐹 Fn 𝐴) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8	7	ancoms 265	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
9		dff1o4 5296	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
10		dff1o4 5296	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
11	8, 9, 10	3imtr4i 200	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1296  ^◡ccnv 4466  Rel wrel 4472   Fn wfn 5044  –1-1-onto→wf1o 5048

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868  df-opab 3922  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-fun 5051  df-fn 5052  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056

This theorem is referenced by:  f1ocnvb  5302  f1orescnv  5304  f1imacnv  5305  f1cnv  5312  f1ococnv1  5317  f1oresrab  5502  f1ocnvfv2  5595  f1ocnvdm  5598  f1ocnvfvrneq  5599  fcof1o  5606  isocnv  5628  f1ofveu  5678  mapsnf1o3  6494  ener  6576  en0  6592  en1  6596  mapen  6642  ssenen  6647  preimaf1ofi  6740  ordiso2  6808  caseinl  6862  enomnilem  6881  fnn0nninf  9992  0tonninf  9994  1tonninf  9995  iseqf1olemkle  10050  iseqf1olemklt  10051  iseqf1olemqcl  10052  iseqf1olemnab  10054  iseqf1olemmo  10058  iseqf1olemqk  10060  seq3f1olemqsumkj  10064  seq3f1olemqsumk  10065  seq3f1olemstep  10067  hashfz1  10322  hashfacen  10372  seq3coll  10378  cnrecnv  10475  isummolemnm  10938  summodclem3  10939  summodclem2a  10940  sqpweven  11596  2sqpwodd  11597  phimullem  11644  xpnnen  11650  exmidsbthrlem  12633