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

Theorem f1ocnvfv2 6084
Description: The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
Assertion
Ref Expression
f1ocnvfv2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( F `  ( `' F `  C ) )  =  C )

Proof of Theorem f1ocnvfv2
StepHypRef Expression
1 f1ococnv2 5750 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( F  o.  `' F )  =  (  _I  |`  B )
)
21fveq1d 5776 . . 3  |-  ( F : A -1-1-onto-> B  ->  ( ( F  o.  `' F
) `  C )  =  ( (  _I  |`  B ) `  C
) )
32adantr 463 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( (  _I  |`  B ) `  C ) )
4 f1ocnv 5736 . . . 4  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
5 f1of 5724 . . . 4  |-  ( `' F : B -1-1-onto-> A  ->  `' F : B --> A )
64, 5syl 16 . . 3  |-  ( F : A -1-1-onto-> B  ->  `' F : B --> A )
7 fvco3 5851 . . 3  |-  ( ( `' F : B --> A  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
86, 7sylan 469 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
9 fvresi 5999 . . 3  |-  ( C  e.  B  ->  (
(  _I  |`  B ) `
 C )  =  C )
109adantl 464 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( (  _I  |`  B ) `
 C )  =  C )
113, 8, 103eqtr3d 2431 1  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( F `  ( `' F `  C ) )  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399    e. wcel 1826    _I cid 4704   `'ccnv 4912    |` cres 4915    o. ccom 4917   -->wf 5492   -1-1-onto->wf1o 5495   ` cfv 5496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504
This theorem is referenced by:  f1ocnvfvb  6086  fveqf1o  6106  isocnv  6127  f1oiso2  6149  weniso  6151  ordiso2  7855  cantnfle  8003  cantnfp1lem3  8012  cantnflem1b  8018  cantnflem1d  8020  cantnflem1  8021  cantnfleOLD  8033  cantnfp1lem3OLD  8038  cantnflem1bOLD  8041  cantnflem1dOLD  8043  cantnflem1OLD  8044  cnfcom2lem  8058  cnfcom2  8059  cnfcom3lem  8060  cnfcom2lemOLD  8066  cnfcom2OLD  8067  cnfcom3lemOLD  8068  acndom2  8348  iunfictbso  8408  ttukeylem7  8808  fpwwe2lem6  8924  fpwwe2lem7  8925  uzrdglem  11971  uzrdgsuci  11974  fzennn  11981  axdc4uzlem  11995  seqf1olem1  12049  seqf1olem2  12050  hashfz1  12321  seqcoll  12416  seqcoll2  12417  summolem3  13538  summolem2a  13539  ackbijnn  13642  prodmolem3  13742  prodmolem2a  13743  sadcaddlem  14109  sadaddlem  14118  sadasslem  14122  sadeq  14124  phimullem  14311  eulerthlem2  14314  catcisolem  15502  mhmf1o  16093  ghmf1o  16413  f1omvdconj  16588  gsumval3eu  17024  gsumval3OLD  17025  gsumval3  17028  lmhmf1o  17805  fidomndrnglem  18068  basqtop  20297  tgqtop  20298  ordthmeolem  20387  symgtgp  20685  imasf1obl  21076  xrhmeo  21531  ovoliunlem2  21999  vitalilem2  22103  dvcnvlem  22462  dvcnv  22463  dvcnvre  22505  efif1olem4  23017  eff1olem  23020  eflog  23049  dvrelog  23105  dvlog  23119  asinrebnd  23348  sqff1o  23573  lgsqrlem4  23736  cnvmot  24048  f1otrg  24295  f1otrge  24296  axcontlem10  24397  nbgracnvfv  24561  cusgrares  24593  usgra2adedgspthlem1  24732  constr3trllem5  24775  cusconngra  24797  wlkiswwlk2lem4  24815  clwlkisclwwlklem2a4  24905  2pthfrgra  25132  cnvunop  26953  unopadj  26954  bracnvbra  27148  abliso  27839  mndpluscn  28062  cvmfolem  28913  cvmliftlem6  28924  f1ocan1fv  30383  ismtycnv  30464  ismtyima  30465  ismtybndlem  30468  rngoisocnv  30550  rmxyval  31016  usgra2adedglem1  32674  mgmhmf1o  32793  lautcnvle  36226  lautcvr  36229  lautj  36230  lautm  36231  ltrncnvatb  36275  ltrncnvel  36279  ltrncnv  36283  ltrneq2  36285  cdlemg17h  36807  diainN  37197  diasslssN  37199  doca3N  37267  dihcnvid2  37413  dochocss  37506  mapdcnvid2  37797
  Copyright terms: Public domain W3C validator