Theorem isof1o 6011

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 5422	. 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 2710   class class class wbr 4287   -1-1-onto->wf1o 5412   ` cfv 5413   Isom wiso 5414

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 5422

This theorem is referenced by:  isores1  6020  isomin  6023  isoini  6024  isoini2  6025  isofrlem  6026  isoselem  6027  isofr  6028  isose  6029  isofr2  6030  isopolem  6031  isosolem  6033  weniso  6040  weisoeq  6041  weisoeq2  6042  wemoiso  6557  wemoiso2  6558  smoiso  6815  smoiso2  6822  supisolem  7712  supisoex  7713  supiso  7714  ordiso2  7721  ordtypelem10  7733  oiexg  7741  oien  7744  oismo  7746  cantnfle  7871  cantnflt2  7873  cantnfp1lem3  7880  cantnflem1b  7886  cantnflem1d  7888  cantnflem1  7889  cantnffval2  7895  cantnfleOLD  7901  cantnflt2OLD  7903  cantnfp1lem3OLD  7906  cantnflem1bOLD  7909  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnffval2OLD  7917  cantnff1o  7918  wemapwe  7920  wemapweOLD  7921  cnfcom3lem  7928  cnfcom3lemOLD  7936  infxpenlem  8172  iunfictbso  8276  dfac12lem2  8305  cofsmo  8430  isf34lem3  8536  isf34lem5  8539  hsmexlem1  8587  fpwwe2lem6  8794  fpwwe2lem7  8795  fpwwe2lem9  8797  pwfseqlem5  8822  fz1isolem  12206  seqcoll  12208  seqcoll2  12209  isercolllem2  13135  isercoll  13137  summolem2a  13184  gsumval3OLD  16373  gsumval3lem1  16374  gsumval3  16376  ordthmeolem  19349  dvne0f1  21459  dvcvx  21467  isoun  25948  erdsze2lem1  27043  prodmolem2a  27398