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

Theorem f1ocnvfv1 7025
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 6634 . . . 4 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐴))
21fveq1d 6663 . . 3 (𝐹:𝐴1-1-onto𝐵 → ((𝐹𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶))
32adantr 484 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → ((𝐹𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶))
4 f1of 6606 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
5 fvco3 6751 . . 3 ((𝐹:𝐴𝐵𝐶𝐴) → ((𝐹𝐹)‘𝐶) = (𝐹‘(𝐹𝐶)))
64, 5sylan 583 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → ((𝐹𝐹)‘𝐶) = (𝐹‘(𝐹𝐶)))
7 fvresi 6926 . . 3 (𝐶𝐴 → (( I ↾ 𝐴)‘𝐶) = 𝐶)
87adantl 485 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → (( I ↾ 𝐴)‘𝐶) = 𝐶)
93, 6, 83eqtr3d 2867 1 ((𝐹:𝐴1-1-onto𝐵𝐶𝐴) → (𝐹‘(𝐹𝐶)) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2115   I cid 5446  ccnv 5541  cres 5544  ccom 5546  wf 6339  1-1-ontowf1o 6342  cfv 6343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351
This theorem is referenced by:  f1ocnvfv  7027  wemapwe  9157  fseqenlem2  9449  acndom  9475  isf34lem5  9798  axcc3  9858  pwfseqlem1  10078  hashdom  13745  fz1isolem  13824  cnrecnv  14524  sadcadd  15805  sadadd2  15807  invinv  17040  catcisolem  17366  mhmf1o  17966  srngnvl  19627  mdetleib2  21197  2ndcdisj  22064  cnheiborlem  23562  iunmbl2  24164  dvcnvlem  24582  eff1olem  25143  logef  25176  adjbdlnb  29870  cnvbrabra  29898  fsumiunle  30556  fzto1stinvn  30778  cycpmfv1  30787  cycpmfv2  30788  cycpmco2lem7  30806  madjusmdetlem1  31152  tpr2rico  31212  esumiun  31410  lautj  37334  lautm  37335  ldilcnv  37356  ltrneq2  37389  trlcnv  37406  diaocN  38366  dihcnvid1  38513  dochocss  38607  mapdcnvid1N  38895  isomushgr  44270
  Copyright terms: Public domain W3C validator