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

Theorem f1ocnvfv2 5982
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 5669 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( F  o.  `' F )  =  (  _I  |`  B )
)
21fveq1d 5697 . . 3  |-  ( F : A -1-1-onto-> B  ->  ( ( F  o.  `' F
) `  C )  =  ( (  _I  |`  B ) `  C
) )
32adantr 452 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( (  _I  |`  B ) `  C ) )
4 f1ocnv 5654 . . . 4  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
5 f1of 5641 . . . 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 5767 . . 3  |-  ( ( `' F : B --> A  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
86, 7sylan 458 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
9 fvresi 5891 . . 3  |-  ( C  e.  B  ->  (
(  _I  |`  B ) `
 C )  =  C )
109adantl 453 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( (  _I  |`  B ) `
 C )  =  C )
113, 8, 103eqtr3d 2452 1  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( F `  ( `' F `  C ) )  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721    _I cid 4461   `'ccnv 4844    |` cres 4847    o. ccom 4849   -->wf 5417   -1-1-onto->wf1o 5420   ` cfv 5421
This theorem is referenced by:  f1ocnvfvb  5984  fveqf1o  5996  isocnv  6017  f1oiso2  6039  weniso  6042  ordiso2  7448  cantnfle  7590  cantnfp1lem3  7600  cantnflem1b  7606  cantnflem1d  7608  cantnflem1  7609  cnfcom2lem  7622  cnfcom2  7623  cnfcom3lem  7624  acndom2  7899  iunfictbso  7959  ttukeylem7  8359  fpwwe2lem6  8474  fpwwe2lem7  8475  uzrdglem  11260  uzrdgsuci  11263  fzennn  11270  axdc4uzlem  11284  seqf1olem1  11325  seqf1olem2  11326  hashfz1  11593  seqcoll  11675  seqcoll2  11676  summolem3  12471  summolem2a  12472  ackbijnn  12570  sadcaddlem  12932  sadaddlem  12941  sadasslem  12945  sadeq  12947  phimullem  13131  eulerthlem2  13134  catcisolem  14224  ghmf1o  14998  gsumval3eu  15476  gsumval3  15477  lmhmf1o  16085  fidomndrnglem  16329  basqtop  17704  tgqtop  17705  ordthmeolem  17794  symgtgp  18092  imasf1obl  18479  xrhmeo  18932  ovoliunlem2  19360  vitalilem2  19462  dvcnvlem  19821  dvcnv  19822  dvcnvre  19864  efif1olem4  20408  eff1olem  20411  eflog  20435  dvrelog  20489  dvlog  20503  asinrebnd  20702  sqff1o  20926  lgsqrlem4  21089  nbgracnvfv  21411  cusgrares  21442  constr3trllem5  21602  cusconngra  21624  cnvunop  23382  unopadj  23383  bracnvbra  23577  mndpluscn  24273  cvmfolem  24927  cvmliftlem6  24938  prodmolem3  25220  prodmolem2a  25221  axcontlem10  25824  f1ocan1fv  26326  ismtycnv  26409  ismtyima  26410  ismtybndlem  26413  rngoisocnv  26495  rmxyval  26876  f1omvdconj  27265  usgra2adedgspthlem1  28051  usgra2adedglem1  28056  2pthfrgra  28123  lautcnvle  30583  lautcvr  30586  lautj  30587  lautm  30588  ltrncnvatb  30632  ltrncnvel  30636  ltrncnv  30640  ltrneq2  30642  cdlemg17h  31162  diainN  31552  diasslssN  31554  doca3N  31622  dihcnvid2  31768  dochocss  31861  mapdcnvid2  32152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429
  Copyright terms: Public domain W3C validator