ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1ocnv GIF version

Theorem f1ocnv 5170
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
StepHypRef Expression
1 fnrel 5028 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel2 4801 . . . . . 6 (Rel 𝐹𝐹 = 𝐹)
3 fneq1 5018 . . . . . . 7 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
43biimprd 156 . . . . . 6 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
52, 4sylbi 119 . . . . 5 (Rel 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
61, 5mpcom 36 . . . 4 (𝐹 Fn 𝐴𝐹 Fn 𝐴)
76anim2i 334 . . 3 ((𝐹 Fn 𝐵𝐹 Fn 𝐴) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
87ancoms 264 . 2 ((𝐹 Fn 𝐴𝐹 Fn 𝐵) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
9 dff1o4 5165 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
10 dff1o4 5165 . 2 (𝐹:𝐵1-1-onto𝐴 ↔ (𝐹 Fn 𝐵𝐹 Fn 𝐴))
118, 9, 103imtr4i 199 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1285  ccnv 4370  Rel wrel 4376   Fn wfn 4927  1-1-ontowf1o 4931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-pow 3956  ax-pr 3972
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-pw 3392  df-sn 3412  df-pr 3413  df-op 3415  df-br 3794  df-opab 3848  df-xp 4377  df-rel 4378  df-cnv 4379  df-co 4380  df-dm 4381  df-rn 4382  df-fun 4934  df-fn 4935  df-f 4936  df-f1 4937  df-fo 4938  df-f1o 4939
This theorem is referenced by:  f1ocnvb  5171  f1orescnv  5173  f1imacnv  5174  f1cnv  5181  f1ococnv1  5186  f1oresrab  5361  f1ocnvfv2  5449  f1ocnvdm  5452  f1ocnvfvrneq  5453  fcof1o  5460  isocnv  5482  f1ofveu  5531  ener  6326  en0  6342  en1  6346  ordiso2  6505  sizefz1  9807  cnrecnv  9935  sqpweven  10697  2sqpwodd  10698  xpnnen  10705
  Copyright terms: Public domain W3C validator