Theorem isof1o 6003

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 5415	. 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 457	1 |- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )

Syntax hints:   -> wi 4   <-> wb 184   A.wral 2705   class class class wbr 4280   -1-1-onto->wf1o 5405   ` cfv 5406   Isom wiso 5407

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 5415

This theorem is referenced by:  isores1  6012  isomin  6015  isoini  6016  isoini2  6017  isofrlem  6018  isoselem  6019  isofr  6020  isose  6021  isofr2  6022  isopolem  6023  isosolem  6025  weniso  6032  weisoeq  6033  weisoeq2  6034  wemoiso  6551  wemoiso2  6552  smoiso  6809  smoiso2  6816  supisolem  7708  supisoex  7709  supiso  7710  ordiso2  7717  ordtypelem10  7729  oiexg  7737  oien  7740  oismo  7742  cantnfle  7867  cantnflt2  7869  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1d  7884  cantnflem1  7885  cantnffval2  7891  cantnfleOLD  7897  cantnflt2OLD  7899  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnffval2OLD  7913  cantnff1o  7914  wemapwe  7916  wemapweOLD  7917  cnfcom3lem  7924  cnfcom3lemOLD  7932  infxpenlem  8168  iunfictbso  8272  dfac12lem2  8301  cofsmo  8426  isf34lem3  8532  isf34lem5  8535  hsmexlem1  8583  fpwwe2lem6  8789  fpwwe2lem7  8790  fpwwe2lem9  8792  pwfseqlem5  8817  fz1isolem  12197  seqcoll  12199  seqcoll2  12200  isercolllem2  13126  isercoll  13128  summolem2a  13175  gsumval3OLD  16361  gsumval3lem1  16362  gsumval3  16364  ordthmeolem  19215  dvne0f1  21325  dvcvx  21333  isoun  25820  erdsze2lem1  26938  prodmolem2a  27293