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

Theorem f1ocnvfv2 5793
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 5500 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( F  o.  `' F )  =  (  _I  |`  B )
)
21fveq1d 5527 . . 3  |-  ( F : A -1-1-onto-> B  ->  ( ( F  o.  `' F
) `  C )  =  ( (  _I  |`  B ) `  C
) )
32adantr 451 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( (  _I  |`  B ) `  C ) )
4 f1ocnv 5485 . . . 4  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
5 f1of 5472 . . . 4  |-  ( `' F : B -1-1-onto-> A  ->  `' F : B --> A )
64, 5syl 15 . . 3  |-  ( F : A -1-1-onto-> B  ->  `' F : B --> A )
7 fvco3 5596 . . 3  |-  ( ( `' F : B --> A  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
86, 7sylan 457 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
9 fvresi 5711 . . 3  |-  ( C  e.  B  ->  (
(  _I  |`  B ) `
 C )  =  C )
109adantl 452 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( (  _I  |`  B ) `
 C )  =  C )
113, 8, 103eqtr3d 2323 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 358    = wceq 1623    e. wcel 1684    _I cid 4304   `'ccnv 4688    |` cres 4691    o. ccom 4693   -->wf 5251   -1-1-onto->wf1o 5254   ` cfv 5255
This theorem is referenced by:  f1ocnvfvb  5795  fveqf1o  5806  isocnv  5827  f1oiso2  5849  weniso  5852  ordiso2  7230  cantnfle  7372  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cnfcom2lem  7404  cnfcom2  7405  cnfcom3lem  7406  acndom2  7681  iunfictbso  7741  ttukeylem7  8142  fpwwe2lem6  8257  fpwwe2lem7  8258  uzrdglem  11020  uzrdgsuci  11023  fzennn  11030  axdc4uzlem  11044  seqf1olem1  11085  seqf1olem2  11086  hashfz1  11345  seqcoll  11401  seqcoll2  11402  summolem3  12187  summolem2a  12188  ackbijnn  12286  sadcaddlem  12648  sadaddlem  12657  sadasslem  12661  sadeq  12663  phimullem  12847  eulerthlem2  12850  catcisolem  13938  ghmf1o  14712  gsumval3eu  15190  gsumval3  15191  lmhmf1o  15803  fidomndrnglem  16047  basqtop  17402  tgqtop  17403  ordthmeolem  17492  symgtgp  17784  imasf1obl  18034  xrhmeo  18444  ovoliunlem2  18862  vitalilem2  18964  dvcnvlem  19323  dvcnv  19324  dvcnvre  19366  efif1olem4  19907  eff1olem  19910  eflog  19933  dvrelog  19984  dvlog  19998  asinrebnd  20197  sqff1o  20420  lgsqrlem4  20583  cnvunop  22498  unopadj  22499  bracnvbra  22693  mndpluscn  23299  cvmfolem  23810  cvmliftlem6  23821  axcontlem10  24601  oriso  25214  f1ocan1fv  26394  ismtycnv  26526  ismtyima  26527  ismtybndlem  26530  rngoisocnv  26612  rmxyval  27000  f1omvdconj  27389  lautcnvle  30278  lautcvr  30281  lautj  30282  lautm  30283  ltrncnvatb  30327  ltrncnvel  30331  ltrncnv  30335  ltrneq2  30337  cdlemg17h  30857  diainN  31247  diasslssN  31249  doca3N  31317  dihcnvid2  31463  dochocss  31556  mapdcnvid2  31847
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263
  Copyright terms: Public domain W3C validator