Theorem isof1o 6234

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

Syntax hints:   -> wi 4   <-> wb 189   A.wral 2756   class class class wbr 4395   -1-1-onto->wf1o 5588   ` cfv 5589   Isom wiso 5590

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 190  df-an 378  df-isom 5598

This theorem is referenced by:  isores1  6243  isomin  6246  isoini  6247  isoini2  6248  isofrlem  6249  isoselem  6250  isofr  6251  isose  6252  isofr2  6253  isopolem  6254  isosolem  6256  weniso  6263  weisoeq  6264  weisoeq2  6265  wemoiso  6797  wemoiso2  6798  smoiso  7099  smoiso2  7106  supisolem  8007  supisoex  8008  supiso  8009  ordiso2  8048  ordtypelem10  8060  oiexg  8068  oien  8071  oismo  8073  cantnfle  8194  cantnflt2  8196  cantnfp1lem3  8203  cantnflem1b  8209  cantnflem1d  8211  cantnflem1  8212  cantnffval2  8218  cantnff1o  8219  wemapwe  8220  cnfcom3lem  8226  infxpenlem  8462  iunfictbso  8563  dfac12lem2  8592  cofsmo  8717  isf34lem3  8823  isf34lem5  8826  hsmexlem1  8874  fpwwe2lem6  9078  fpwwe2lem7  9079  fpwwe2lem9  9081  pwfseqlem5  9106  fz1isolem  12665  seqcoll  12668  seqcoll2  12669  isercolllem2  13806  isercoll  13808  summolem2a  13858  prodmolem2a  14065  gsumval3lem1  17617  gsumval3  17619  ordthmeolem  20893  dvne0f1  23043  dvcvx  23051  isoun  28357  erdsze2lem1  29998  fourierdlem20  38101  fourierdlem50  38132  fourierdlem51  38133  fourierdlem52  38134  fourierdlem63  38145  fourierdlem64  38146  fourierdlem65  38147  fourierdlem76  38158  fourierdlem102  38184  fourierdlem114  38196