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

Theorem f1ocnvfv2 5974
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 5661 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( F  o.  `' F )  =  (  _I  |`  B )
)
21fveq1d 5689 . . 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 5646 . . . 4  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
5 f1of 5633 . . . 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 5759 . . 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 5883 . . 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 2444 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 4453   `'ccnv 4836    |` cres 4839    o. ccom 4841   -->wf 5409   -1-1-onto->wf1o 5412   ` cfv 5413
This theorem is referenced by:  f1ocnvfvb  5976  fveqf1o  5988  isocnv  6009  f1oiso2  6031  weniso  6034  ordiso2  7440  cantnfle  7582  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  cnfcom2lem  7614  cnfcom2  7615  cnfcom3lem  7616  acndom2  7891  iunfictbso  7951  ttukeylem7  8351  fpwwe2lem6  8466  fpwwe2lem7  8467  uzrdglem  11252  uzrdgsuci  11255  fzennn  11262  axdc4uzlem  11276  seqf1olem1  11317  seqf1olem2  11318  hashfz1  11585  seqcoll  11667  seqcoll2  11668  summolem3  12463  summolem2a  12464  ackbijnn  12562  sadcaddlem  12924  sadaddlem  12933  sadasslem  12937  sadeq  12939  phimullem  13123  eulerthlem2  13126  catcisolem  14216  ghmf1o  14990  gsumval3eu  15468  gsumval3  15469  lmhmf1o  16077  fidomndrnglem  16321  basqtop  17696  tgqtop  17697  ordthmeolem  17786  symgtgp  18084  imasf1obl  18471  xrhmeo  18924  ovoliunlem2  19352  vitalilem2  19454  dvcnvlem  19813  dvcnv  19814  dvcnvre  19856  efif1olem4  20400  eff1olem  20403  eflog  20427  dvrelog  20481  dvlog  20495  asinrebnd  20694  sqff1o  20918  lgsqrlem4  21081  nbgracnvfv  21403  cusgrares  21434  constr3trllem5  21594  cusconngra  21616  cnvunop  23374  unopadj  23375  bracnvbra  23569  mndpluscn  24265  cvmfolem  24919  cvmliftlem6  24930  prodmolem3  25212  prodmolem2a  25213  axcontlem10  25816  f1ocan1fv  26318  ismtycnv  26401  ismtyima  26402  ismtybndlem  26405  rngoisocnv  26487  rmxyval  26868  f1omvdconj  27257  usgra2adedgspthlem1  28043  usgra2adedglem1  28048  2pthfrgra  28115  lautcnvle  30571  lautcvr  30574  lautj  30575  lautm  30576  ltrncnvatb  30620  ltrncnvel  30624  ltrncnv  30628  ltrneq2  30630  cdlemg17h  31150  diainN  31540  diasslssN  31542  doca3N  31610  dihcnvid2  31756  dochocss  31849  mapdcnvid2  32140
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 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421
  Copyright terms: Public domain W3C validator