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

Theorem f1ocnvfv2 5981
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 5664 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( F  o.  `' F )  =  (  _I  |`  B )
)
21fveq1d 5690 . . 3  |-  ( F : A -1-1-onto-> B  ->  ( ( F  o.  `' F
) `  C )  =  ( (  _I  |`  B ) `  C
) )
32adantr 462 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( (  _I  |`  B ) `  C ) )
4 f1ocnv 5650 . . . 4  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
5 f1of 5638 . . . 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 5765 . . 3  |-  ( ( `' F : B --> A  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
86, 7sylan 468 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
9 fvresi 5901 . . 3  |-  ( C  e.  B  ->  (
(  _I  |`  B ) `
 C )  =  C )
109adantl 463 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( (  _I  |`  B ) `
 C )  =  C )
113, 8, 103eqtr3d 2481 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 369    = wceq 1364    e. wcel 1761    _I cid 4627   `'ccnv 4835    |` cres 4838    o. ccom 4840   -->wf 5411   -1-1-onto->wf1o 5414   ` cfv 5415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423
This theorem is referenced by:  f1ocnvfvb  5983  fveqf1o  5997  isocnv  6018  f1oiso2  6040  weniso  6042  ordiso2  7725  cantnfle  7875  cantnfp1lem3  7884  cantnflem1b  7890  cantnflem1d  7892  cantnflem1  7893  cantnfleOLD  7905  cantnfp1lem3OLD  7910  cantnflem1bOLD  7913  cantnflem1dOLD  7915  cantnflem1OLD  7916  cnfcom2lem  7930  cnfcom2  7931  cnfcom3lem  7932  cnfcom2lemOLD  7938  cnfcom2OLD  7939  cnfcom3lemOLD  7940  acndom2  8220  iunfictbso  8280  ttukeylem7  8680  fpwwe2lem6  8798  fpwwe2lem7  8799  uzrdglem  11776  uzrdgsuci  11779  fzennn  11786  axdc4uzlem  11800  seqf1olem1  11841  seqf1olem2  11842  hashfz1  12113  seqcoll  12212  seqcoll2  12213  summolem3  13187  summolem2a  13188  ackbijnn  13287  sadcaddlem  13649  sadaddlem  13658  sadasslem  13662  sadeq  13664  phimullem  13850  eulerthlem2  13853  catcisolem  14970  ghmf1o  15769  f1omvdconj  15945  gsumval3eu  16374  gsumval3OLD  16375  gsumval3  16378  lmhmf1o  17105  fidomndrnglem  17356  basqtop  19243  tgqtop  19244  ordthmeolem  19333  symgtgp  19631  imasf1obl  20022  xrhmeo  20477  ovoliunlem2  20945  vitalilem2  21048  dvcnvlem  21407  dvcnv  21408  dvcnvre  21450  efif1olem4  21960  eff1olem  21963  eflog  21987  dvrelog  22041  dvlog  22055  asinrebnd  22255  sqff1o  22479  lgsqrlem4  22642  f1otrg  23052  f1otrge  23053  axcontlem10  23154  nbgracnvfv  23284  cusgrares  23315  constr3trllem5  23475  cusconngra  23497  cnvunop  25257  unopadj  25258  bracnvbra  25452  abliso  26092  mndpluscn  26292  cvmfolem  27098  cvmliftlem6  27109  prodmolem3  27375  prodmolem2a  27376  f1ocan1fv  28545  ismtycnv  28626  ismtyima  28627  ismtybndlem  28630  rngoisocnv  28712  rmxyval  29181  usgra2adedgspthlem1  30228  usgra2adedglem1  30233  wlkiswwlk2lem4  30253  clwlkisclwwlklem2a4  30371  2pthfrgra  30528  lautcnvle  33455  lautcvr  33458  lautj  33459  lautm  33460  ltrncnvatb  33504  ltrncnvel  33508  ltrncnv  33512  ltrneq2  33514  cdlemg17h  34034  diainN  34424  diasslssN  34426  doca3N  34494  dihcnvid2  34640  dochocss  34733  mapdcnvid2  35024
  Copyright terms: Public domain W3C validator