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

Theorem f1ocnvfv2 5915
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 5606 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( F  o.  `' F )  =  (  _I  |`  B )
)
21fveq1d 5634 . . 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 5591 . . . 4  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
5 f1of 5578 . . . 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 5703 . . 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 5824 . . 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 2406 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 1647    e. wcel 1715    _I cid 4407   `'ccnv 4791    |` cres 4794    o. ccom 4796   -->wf 5354   -1-1-onto->wf1o 5357   ` cfv 5358
This theorem is referenced by:  f1ocnvfvb  5917  fveqf1o  5929  isocnv  5950  f1oiso2  5972  weniso  5975  ordiso2  7377  cantnfle  7519  cantnfp1lem3  7529  cantnflem1b  7535  cantnflem1d  7537  cantnflem1  7538  cnfcom2lem  7551  cnfcom2  7552  cnfcom3lem  7553  acndom2  7828  iunfictbso  7888  ttukeylem7  8289  fpwwe2lem6  8404  fpwwe2lem7  8405  uzrdglem  11184  uzrdgsuci  11187  fzennn  11194  axdc4uzlem  11208  seqf1olem1  11249  seqf1olem2  11250  hashfz1  11517  seqcoll  11599  seqcoll2  11600  summolem3  12395  summolem2a  12396  ackbijnn  12494  sadcaddlem  12856  sadaddlem  12865  sadasslem  12869  sadeq  12871  phimullem  13055  eulerthlem2  13058  catcisolem  14148  ghmf1o  14922  gsumval3eu  15400  gsumval3  15401  lmhmf1o  16013  fidomndrnglem  16257  basqtop  17619  tgqtop  17620  ordthmeolem  17709  symgtgp  17997  imasf1obl  18247  xrhmeo  18659  ovoliunlem2  19077  vitalilem2  19179  dvcnvlem  19538  dvcnv  19539  dvcnvre  19581  efif1olem4  20125  eff1olem  20128  eflog  20152  dvrelog  20206  dvlog  20220  asinrebnd  20419  sqff1o  20643  lgsqrlem4  20806  cnvunop  22811  unopadj  22812  bracnvbra  23006  mndpluscn  23667  cvmfolem  24413  cvmliftlem6  24424  prodmolem3  24743  prodmolem2a  24744  axcontlem10  25343  f1ocan1fv  25901  ismtycnv  26032  ismtyima  26033  ismtybndlem  26036  rngoisocnv  26118  rmxyval  26506  f1omvdconj  26895  nbgracnvfv  27606  cusgrares  27637  constr3trllem5  27780  cusconngra  27802  2pthfrgra  27846  lautcnvle  30349  lautcvr  30352  lautj  30353  lautm  30354  ltrncnvatb  30398  ltrncnvel  30402  ltrncnv  30406  ltrneq2  30408  cdlemg17h  30928  diainN  31318  diasslssN  31320  doca3N  31388  dihcnvid2  31534  dochocss  31627  mapdcnvid2  31918
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-sbc 3078  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-id 4412  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366
  Copyright terms: Public domain W3C validator