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

Theorem f1ocnvfv2 5996
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 5679 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( F  o.  `' F )  =  (  _I  |`  B )
)
21fveq1d 5705 . . 3  |-  ( F : A -1-1-onto-> B  ->  ( ( F  o.  `' F
) `  C )  =  ( (  _I  |`  B ) `  C
) )
32adantr 465 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( (  _I  |`  B ) `  C ) )
4 f1ocnv 5665 . . . 4  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
5 f1of 5653 . . . 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 5780 . . 3  |-  ( ( `' F : B --> A  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
86, 7sylan 471 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( ( F  o.  `' F ) `  C
)  =  ( F `
 ( `' F `  C ) ) )
9 fvresi 5916 . . 3  |-  ( C  e.  B  ->  (
(  _I  |`  B ) `
 C )  =  C )
109adantl 466 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( (  _I  |`  B ) `
 C )  =  C )
113, 8, 103eqtr3d 2483 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 1369    e. wcel 1756    _I cid 4643   `'ccnv 4851    |` cres 4854    o. ccom 4856   -->wf 5426   -1-1-onto->wf1o 5429   ` cfv 5430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438
This theorem is referenced by:  f1ocnvfvb  5998  fveqf1o  6012  isocnv  6033  f1oiso2  6055  weniso  6057  ordiso2  7741  cantnfle  7891  cantnfp1lem3  7900  cantnflem1b  7906  cantnflem1d  7908  cantnflem1  7909  cantnfleOLD  7921  cantnfp1lem3OLD  7926  cantnflem1bOLD  7929  cantnflem1dOLD  7931  cantnflem1OLD  7932  cnfcom2lem  7946  cnfcom2  7947  cnfcom3lem  7948  cnfcom2lemOLD  7954  cnfcom2OLD  7955  cnfcom3lemOLD  7956  acndom2  8236  iunfictbso  8296  ttukeylem7  8696  fpwwe2lem6  8814  fpwwe2lem7  8815  uzrdglem  11792  uzrdgsuci  11795  fzennn  11802  axdc4uzlem  11816  seqf1olem1  11857  seqf1olem2  11858  hashfz1  12129  seqcoll  12228  seqcoll2  12229  summolem3  13203  summolem2a  13204  ackbijnn  13303  sadcaddlem  13665  sadaddlem  13674  sadasslem  13678  sadeq  13680  phimullem  13866  eulerthlem2  13869  catcisolem  14986  mhmf1o  15485  ghmf1o  15788  f1omvdconj  15964  gsumval3eu  16393  gsumval3OLD  16394  gsumval3  16397  lmhmf1o  17139  fidomndrnglem  17390  basqtop  19296  tgqtop  19297  ordthmeolem  19386  symgtgp  19684  imasf1obl  20075  xrhmeo  20530  ovoliunlem2  20998  vitalilem2  21101  dvcnvlem  21460  dvcnv  21461  dvcnvre  21503  efif1olem4  22013  eff1olem  22016  eflog  22040  dvrelog  22094  dvlog  22108  asinrebnd  22308  sqff1o  22532  lgsqrlem4  22695  f1otrg  23129  f1otrge  23130  axcontlem10  23231  nbgracnvfv  23361  cusgrares  23392  constr3trllem5  23552  cusconngra  23574  cnvunop  25334  unopadj  25335  bracnvbra  25529  abliso  26171  mndpluscn  26368  cvmfolem  27180  cvmliftlem6  27191  prodmolem3  27458  prodmolem2a  27459  f1ocan1fv  28632  ismtycnv  28713  ismtyima  28714  ismtybndlem  28717  rngoisocnv  28799  rmxyval  29268  usgra2adedgspthlem1  30315  usgra2adedglem1  30320  wlkiswwlk2lem4  30340  clwlkisclwwlklem2a4  30458  2pthfrgra  30615  lautcnvle  33745  lautcvr  33748  lautj  33749  lautm  33750  ltrncnvatb  33794  ltrncnvel  33798  ltrncnv  33802  ltrneq2  33804  cdlemg17h  34324  diainN  34714  diasslssN  34716  doca3N  34784  dihcnvid2  34930  dochocss  35023  mapdcnvid2  35314
  Copyright terms: Public domain W3C validator