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

Theorem f1ocnvfv1 6162
Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
Assertion
Ref Expression
f1ocnvfv1  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( `' F `  ( F `  C ) )  =  C )

Proof of Theorem f1ocnvfv1
StepHypRef Expression
1 f1ococnv1 5826 . . . 4  |-  ( F : A -1-1-onto-> B  ->  ( `' F  o.  F )  =  (  _I  |`  A ) )
21fveq1d 5850 . . 3  |-  ( F : A -1-1-onto-> B  ->  ( ( `' F  o.  F
) `  C )  =  ( (  _I  |`  A ) `  C
) )
32adantr 463 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( ( `' F  o.  F ) `  C
)  =  ( (  _I  |`  A ) `  C ) )
4 f1of 5798 . . 3  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
5 fvco3 5925 . . 3  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( ( `' F  o.  F ) `  C
)  =  ( `' F `  ( F `
 C ) ) )
64, 5sylan 469 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( ( `' F  o.  F ) `  C
)  =  ( `' F `  ( F `
 C ) ) )
7 fvresi 6076 . . 3  |-  ( C  e.  A  ->  (
(  _I  |`  A ) `
 C )  =  C )
87adantl 464 . 2  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( (  _I  |`  A ) `
 C )  =  C )
93, 6, 83eqtr3d 2451 1  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  A )  ->  ( `' F `  ( F `  C ) )  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842    _I cid 4732   `'ccnv 4821    |` cres 4824    o. ccom 4826   -->wf 5564   -1-1-onto->wf1o 5567   ` cfv 5568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576
This theorem is referenced by:  f1ocnvfv  6164  wemapwe  8170  wemapweOLD  8171  fseqenlem2  8437  acndom  8463  isf34lem5  8789  axcc3  8849  pwfseqlem1  9065  hashdom  12493  fz1isolem  12557  cnrecnv  13145  sadcadd  14315  sadadd2  14317  invinv  15381  catcisolem  15707  mhmf1o  16298  srngnvl  17823  mdetleib2  19380  2ndcdisj  20247  cnheiborlem  21744  iunmbl2  22257  dvcnvlem  22667  eff1olem  23225  logef  23259  nbgraf1olem5  24849  adjbdlnb  27402  cnvbrabra  27430  tpr2rico  28333  esumiun  28527  lautj  33090  lautm  33091  ldilcnv  33112  ltrneq2  33145  trlcnv  33163  diaocN  34125  dihcnvid1  34272  dochocss  34366  mapdcnvid1N  34654
  Copyright terms: Public domain W3C validator