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

Theorem isof1o 6214
Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
Assertion
Ref Expression
isof1o  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)

Proof of Theorem isof1o
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-isom 5590 . 2  |-  ( H 
Isom  R ,  S  ( A ,  B )  <-> 
( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) ) )
21simplbi 462 1  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wral 2736   class class class wbr 4401   -1-1-onto->wf1o 5580   ` cfv 5581    Isom wiso 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373  df-isom 5590
This theorem is referenced by:  isores1  6223  isomin  6226  isoini  6227  isoini2  6228  isofrlem  6229  isoselem  6230  isofr  6231  isose  6232  isofr2  6233  isopolem  6234  isosolem  6236  weniso  6243  weisoeq  6244  weisoeq2  6245  wemoiso  6775  wemoiso2  6776  smoiso  7078  smoiso2  7085  supisolem  7986  supisoex  7987  supiso  7988  ordiso2  8027  ordtypelem10  8039  oiexg  8047  oien  8050  oismo  8052  cantnfle  8173  cantnflt2  8175  cantnfp1lem3  8182  cantnflem1b  8188  cantnflem1d  8190  cantnflem1  8191  cantnffval2  8197  cantnff1o  8198  wemapwe  8199  cnfcom3lem  8205  infxpenlem  8441  iunfictbso  8542  dfac12lem2  8571  cofsmo  8696  isf34lem3  8802  isf34lem5  8805  hsmexlem1  8853  fpwwe2lem6  9057  fpwwe2lem7  9058  fpwwe2lem9  9060  pwfseqlem5  9085  fz1isolem  12621  seqcoll  12624  seqcoll2  12625  isercolllem2  13722  isercoll  13724  summolem2a  13774  prodmolem2a  13981  gsumval3lem1  17532  gsumval3  17534  ordthmeolem  20809  dvne0f1  22957  dvcvx  22965  isoun  28275  erdsze2lem1  29919  fourierdlem20  37983  fourierdlem50  38014  fourierdlem51  38015  fourierdlem52  38016  fourierdlem63  38027  fourierdlem64  38028  fourierdlem65  38029  fourierdlem76  38040  fourierdlem102  38066  fourierdlem114  38078
  Copyright terms: Public domain W3C validator