Theorem isof1o 6222

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

Syntax hints:   -> wi 4   <-> wb 187   A.wral 2773   class class class wbr 4417   -1-1-onto->wf1o 5591   ` cfv 5592   Isom wiso 5593

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 188  df-an 372  df-isom 5601

This theorem is referenced by:  isores1  6231  isomin  6234  isoini  6235  isoini2  6236  isofrlem  6237  isoselem  6238  isofr  6239  isose  6240  isofr2  6241  isopolem  6242  isosolem  6244  weniso  6251  weisoeq  6252  weisoeq2  6253  wemoiso  6783  wemoiso2  6784  smoiso  7080  smoiso2  7087  supisolem  7986  supisoex  7987  supiso  7988  ordiso2  8021  ordtypelem10  8033  oiexg  8041  oien  8044  oismo  8046  cantnfle  8166  cantnflt2  8168  cantnfp1lem3  8175  cantnflem1b  8181  cantnflem1d  8183  cantnflem1  8184  cantnffval2  8190  cantnff1o  8191  wemapwe  8192  cnfcom3lem  8198  infxpenlem  8434  iunfictbso  8534  dfac12lem2  8563  cofsmo  8688  isf34lem3  8794  isf34lem5  8797  hsmexlem1  8845  fpwwe2lem6  9049  fpwwe2lem7  9050  fpwwe2lem9  9052  pwfseqlem5  9077  fz1isolem  12608  seqcoll  12610  seqcoll2  12611  isercolllem2  13696  isercoll  13698  summolem2a  13748  prodmolem2a  13955  gsumval3lem1  17467  gsumval3  17469  ordthmeolem  20740  dvne0f1  22838  dvcvx  22846  isoun  28119  erdsze2lem1  29711  fourierdlem20  37562  fourierdlem50  37592  fourierdlem51  37593  fourierdlem52  37594  fourierdlem63  37605  fourierdlem64  37606  fourierdlem65  37607  fourierdlem76  37618  fourierdlem102  37644  fourierdlem114  37656