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

Theorem f1ocnvdm 6186
Description: The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.)
Assertion
Ref Expression
f1ocnvdm  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( `' F `  C )  e.  A
)

Proof of Theorem f1ocnvdm
StepHypRef Expression
1 f1ocnv 5833 . . 3  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
2 f1of 5821 . . 3  |-  ( `' F : B -1-1-onto-> A  ->  `' F : B --> A )
31, 2syl 16 . 2  |-  ( F : A -1-1-onto-> B  ->  `' F : B --> A )
43ffvelrnda 6031 1  |-  ( ( F : A -1-1-onto-> B  /\  C  e.  B )  ->  ( `' F `  C )  e.  A
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   `'ccnv 5003   -->wf 5589   -1-1-onto->wf1o 5592   ` cfv 5593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601
This theorem is referenced by:  f1oiso2  6246  f1ocnvfv3  6290  uzrdglem  12046  uzrdgsuci  12049  fzennn  12056  cardfz  12058  fzfi  12060  iunmbl2  21812  f1otrg  23965  axcontlem10  24067  nbgraf1olem3  24234  nbgraf1olem5  24236  cusgrares  24263  constr3trllem1  24441  wlkiswwlk2lem5  24486  clwlkisclwwlklem2a  24576  cnvbraval  26820  cnvbracl  26821  mndpluscn  27701  ismtycnv  30193  rngoisocnv  30279  rmxyelxp  30744  usgra2adedglem1  32114  lautcnvclN  35177  lautcnvle  35178  lautcvr  35181  lautj  35182  lautm  35183  ltrncnvatb  35227  diacnvclN  36141  dihcnvcl  36361  dihlspsnat  36423  dihglblem6  36430  dochocss  36456  dochnoncon  36481  mapdcnvcl  36742
  Copyright terms: Public domain W3C validator