MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1ocnvfv1 Structured version   Visualization version   GIF version

Theorem f1ocnvfv1 7296
Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
Assertion
Ref Expression
f1ocnvfv1 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → (𝐹‘(𝐹𝐶)) = 𝐶)

Proof of Theorem f1ocnvfv1
StepHypRef Expression
1 f1ococnv1 6878 . . . 4 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
21fveq1d 6909 . . 3 (𝐹:𝐴1-1-onto𝐵 → ((𝐹𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶))
32adantr 480 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → ((𝐹𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶))
4 f1of 6849 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
5 fvco3 7008 . . 3 ((𝐹:𝐴𝐵𝐶𝐴) → ((𝐹𝐹)‘𝐶) = (𝐹‘(𝐹𝐶)))
64, 5sylan 580 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → ((𝐹𝐹)‘𝐶) = (𝐹‘(𝐹𝐶)))
7 fvresi 7193 . . 3 (𝐶𝐴 → (( I ↾ 𝐴)‘𝐶) = 𝐶)
87adantl 481 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → (( I ↾ 𝐴)‘𝐶) = 𝐶)
93, 6, 83eqtr3d 2783 1 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → (𝐹‘(𝐹𝐶)) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106   I cid 5582  ccnv 5688  cres 5691  ccom 5693  wf 6559  1-1-ontowf1o 6562  cfv 6563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571
This theorem is referenced by:  f1ocnvfv  7298  wemapwe  9735  fseqenlem2  10063  acndom  10089  isf34lem5  10416  axcc3  10476  pwfseqlem1  10696  hashdom  14415  fz1isolem  14497  cnrecnv  15201  sadcadd  16492  sadadd2  16494  invinv  17818  catcisolem  18164  mhmf1o  18822  rngisom1  20483  srngnvl  20868  mdetleib2  22610  2ndcdisj  23480  cnheiborlem  25000  iunmbl2  25606  dvcnvlem  26029  eff1olem  26605  logef  26638  adjbdlnb  32113  cnvbrabra  32141  fsumiunle  32836  ccatws1f1o  32921  fzto1stinvn  33107  cycpmfv1  33116  cycpmfv2  33117  cycpmco2lem7  33135  madjusmdetlem1  33788  tpr2rico  33873  esumiun  34075  lautj  40076  lautm  40077  ldilcnv  40098  ltrneq2  40131  trlcnv  40148  diaocN  41108  dihcnvid1  41255  dochocss  41349  mapdcnvid1N  41637  aks6d1c1p3  42092  sticksstones19  42147  nvocnvb  43412  grimcnv  47817  gricushgr  47824  uspgrlimlem2  47892
  Copyright terms: Public domain W3C validator