Theorem isof1o 6207

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 5595	. 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 2814   class class class wbr 4447   -1-1-onto->wf1o 5585   ` cfv 5586   Isom wiso 5587

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 5595

This theorem is referenced by:  isores1  6216  isomin  6219  isoini  6220  isoini2  6221  isofrlem  6222  isoselem  6223  isofr  6224  isose  6225  isofr2  6226  isopolem  6227  isosolem  6229  weniso  6236  weisoeq  6237  weisoeq2  6238  wemoiso  6766  wemoiso2  6767  smoiso  7030  smoiso2  7037  supisolem  7927  supisoex  7928  supiso  7929  ordiso2  7936  ordtypelem10  7948  oiexg  7956  oien  7959  oismo  7961  cantnfle  8086  cantnflt2  8088  cantnfp1lem3  8095  cantnflem1b  8101  cantnflem1d  8103  cantnflem1  8104  cantnffval2  8110  cantnfleOLD  8116  cantnflt2OLD  8118  cantnfp1lem3OLD  8121  cantnflem1bOLD  8124  cantnflem1dOLD  8126  cantnflem1OLD  8127  cantnffval2OLD  8132  cantnff1o  8133  wemapwe  8135  wemapweOLD  8136  cnfcom3lem  8143  cnfcom3lemOLD  8151  infxpenlem  8387  iunfictbso  8491  dfac12lem2  8520  cofsmo  8645  isf34lem3  8751  isf34lem5  8754  hsmexlem1  8802  fpwwe2lem6  9009  fpwwe2lem7  9010  fpwwe2lem9  9012  pwfseqlem5  9037  fz1isolem  12472  seqcoll  12474  seqcoll2  12475  isercolllem2  13447  isercoll  13449  summolem2a  13496  gsumval3OLD  16699  gsumval3lem1  16700  gsumval3  16702  ordthmeolem  20037  dvne0f1  22148  dvcvx  22156  isoun  27192  erdsze2lem1  28287  prodmolem2a  28643  fourierdlem20  31427  fourierdlem50  31457  fourierdlem51  31458  fourierdlem52  31459  fourierdlem63  31470  fourierdlem64  31471  fourierdlem65  31472  fourierdlem76  31483  fourierdlem102  31509  fourierdlem114  31521