Theorem isof1o 6118

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 5528	. 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 2795   class class class wbr 4393   -1-1-onto->wf1o 5518   ` cfv 5519   Isom wiso 5520

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 5528

This theorem is referenced by:  isores1  6127  isomin  6130  isoini  6131  isoini2  6132  isofrlem  6133  isoselem  6134  isofr  6135  isose  6136  isofr2  6137  isopolem  6138  isosolem  6140  weniso  6147  weisoeq  6148  weisoeq2  6149  wemoiso  6665  wemoiso2  6666  smoiso  6926  smoiso2  6933  supisolem  7824  supisoex  7825  supiso  7826  ordiso2  7833  ordtypelem10  7845  oiexg  7853  oien  7856  oismo  7858  cantnfle  7983  cantnflt2  7985  cantnfp1lem3  7992  cantnflem1b  7998  cantnflem1d  8000  cantnflem1  8001  cantnffval2  8007  cantnfleOLD  8013  cantnflt2OLD  8015  cantnfp1lem3OLD  8018  cantnflem1bOLD  8021  cantnflem1dOLD  8023  cantnflem1OLD  8024  cantnffval2OLD  8029  cantnff1o  8030  wemapwe  8032  wemapweOLD  8033  cnfcom3lem  8040  cnfcom3lemOLD  8048  infxpenlem  8284  iunfictbso  8388  dfac12lem2  8417  cofsmo  8542  isf34lem3  8648  isf34lem5  8651  hsmexlem1  8699  fpwwe2lem6  8906  fpwwe2lem7  8907  fpwwe2lem9  8909  pwfseqlem5  8934  fz1isolem  12325  seqcoll  12327  seqcoll2  12328  isercolllem2  13254  isercoll  13256  summolem2a  13303  gsumval3OLD  16495  gsumval3lem1  16496  gsumval3  16498  ordthmeolem  19499  dvne0f1  21610  dvcvx  21618  isoun  26141  erdsze2lem1  27228  prodmolem2a  27584