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

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

Proof of Theorem f1ocnvfv2
StepHypRef Expression
1 f1ococnv2 6122 . . . 4 (𝐹:𝐴1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐵))
21fveq1d 6152 . . 3 (𝐹:𝐴1-1-onto𝐵 → ((𝐹𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
32adantr 481 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐵) → ((𝐹𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4 f1ocnv 6108 . . . 4 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
5 f1of 6096 . . . 4 (𝐹:𝐵1-1-onto𝐴𝐹:𝐵𝐴)
64, 5syl 17 . . 3 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵𝐴)
7 fvco3 6233 . . 3 ((𝐹:𝐵𝐴𝐶𝐵) → ((𝐹𝐹)‘𝐶) = (𝐹‘(𝐹𝐶)))
86, 7sylan 488 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐵) → ((𝐹𝐹)‘𝐶) = (𝐹‘(𝐹𝐶)))
9 fvresi 6394 . . 3 (𝐶𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
109adantl 482 . 2 ((𝐹:𝐴1-1-onto𝐵𝐶𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
113, 8, 103eqtr3d 2668 1 ((𝐹:𝐴1-1-onto𝐵𝐶𝐵) → (𝐹‘(𝐹𝐶)) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1992   I cid 4989  ccnv 5078  cres 5081  ccom 5083  wf 5846  1-1-ontowf1o 5849  cfv 5850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858
This theorem is referenced by:  f1ocnvfvb  6490  fveqf1o  6512  isocnv  6535  f1oiso2  6557  weniso  6559  ordiso2  8365  cantnfle  8513  cantnfp1lem3  8522  cantnflem1b  8528  cantnflem1d  8530  cantnflem1  8531  cnfcom2lem  8543  cnfcom2  8544  cnfcom3lem  8545  acndom2  8822  iunfictbso  8882  ttukeylem7  9282  fpwwe2lem6  9402  fpwwe2lem7  9403  uzrdglem  12693  uzrdgsuci  12696  fzennn  12704  axdc4uzlem  12719  seqf1olem1  12777  seqf1olem2  12778  hashfz1  13071  seqcoll  13183  seqcoll2  13184  summolem3  14373  summolem2a  14374  ackbijnn  14480  prodmolem3  14583  prodmolem2a  14584  sadcaddlem  15098  sadaddlem  15107  sadasslem  15111  sadeq  15113  phimullem  15403  eulerthlem2  15406  catcisolem  16672  mhmf1o  17261  ghmf1o  17606  f1omvdconj  17782  gsumval3eu  18221  gsumval3  18224  lmhmf1o  18960  fidomndrnglem  19220  basqtop  21419  tgqtop  21420  ordthmeolem  21509  symgtgp  21810  imasf1obl  22198  xrhmeo  22648  ovoliunlem2  23173  vitalilem2  23279  dvcnvlem  23638  dvcnv  23639  dvcnvre  23681  efif1olem4  24190  eff1olem  24193  eflog  24222  dvrelog  24278  dvlog  24292  asinrebnd  24523  sqff1o  24803  lgsqrlem4  24969  cnvmot  25331  f1otrg  25646  f1otrge  25647  axcontlem10  25748  usgrnbcnvfv  26148  wlkiswwlks2lem4  26621  clwlkclwwlklem2a4  26759  cnvunop  28617  unopadj  28618  bracnvbra  28812  abliso  29473  mndpluscn  29746  cvmfolem  30961  cvmliftlem6  30972  f1ocan1fv  33139  ismtycnv  33219  ismtyima  33220  ismtybndlem  33223  rngoisocnv  33398  lautcnvle  34841  lautcvr  34844  lautj  34845  lautm  34846  ltrncnvatb  34890  ltrncnvel  34894  ltrncnv  34898  ltrneq2  34900  cdlemg17h  35422  diainN  35812  diasslssN  35814  doca3N  35882  dihcnvid2  36028  dochocss  36121  mapdcnvid2  36412  rmxyval  36946  mgmhmf1o  41048
  Copyright terms: Public domain W3C validator