Theorem isof1o 6206

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.

Step	Hyp	Ref	Expression
1		df-isom 5587	. 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 ) ) ) )
2	1	simplbi 460	1 |- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )

Syntax hints:   -> wi 4   <-> wb 184   A.wral 2793   class class class wbr 4437   -1-1-onto->wf1o 5577   ` cfv 5578   Isom wiso 5579

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 185  df-an 371  df-isom 5587

This theorem is referenced by:  isores1  6215  isomin  6218  isoini  6219  isoini2  6220  isofrlem  6221  isoselem  6222  isofr  6223  isose  6224  isofr2  6225  isopolem  6226  isosolem  6228  weniso  6235  weisoeq  6236  weisoeq2  6237  wemoiso  6770  wemoiso2  6771  smoiso  7035  smoiso2  7042  supisolem  7934  supisoex  7935  supiso  7936  ordiso2  7943  ordtypelem10  7955  oiexg  7963  oien  7966  oismo  7968  cantnfle  8093  cantnflt2  8095  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1d  8110  cantnflem1  8111  cantnffval2  8117  cantnfleOLD  8123  cantnflt2OLD  8125  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnffval2OLD  8139  cantnff1o  8140  wemapwe  8142  wemapweOLD  8143  cnfcom3lem  8150  cnfcom3lemOLD  8158  infxpenlem  8394  iunfictbso  8498  dfac12lem2  8527  cofsmo  8652  isf34lem3  8758  isf34lem5  8761  hsmexlem1  8809  fpwwe2lem6  9016  fpwwe2lem7  9017  fpwwe2lem9  9019  pwfseqlem5  9044  fz1isolem  12491  seqcoll  12493  seqcoll2  12494  isercolllem2  13469  isercoll  13471  summolem2a  13518  prodmolem2a  13722  gsumval3OLD  16886  gsumval3lem1  16887  gsumval3  16889  ordthmeolem  20279  dvne0f1  22390  dvcvx  22398  isoun  27496  erdsze2lem1  28624  fourierdlem20  31798  fourierdlem50  31828  fourierdlem51  31829  fourierdlem52  31830  fourierdlem63  31841  fourierdlem64  31842  fourierdlem65  31843  fourierdlem76  31854  fourierdlem102  31880  fourierdlem114  31892