Theorem isof1o 5958

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

Syntax hints:   -> wi 4   <-> wb 105   A.wral 2511   class class class wbr 4093   -1-1-onto->wf1o 5332   ` cfv 5333   Isom wiso 5334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-isom 5342

This theorem is referenced by:  isocnv2  5963  isores1  5965  isoini  5969  isoini2  5970  isoselem  5971  isose  5972  isopolem  5973  isosolem  5975  smoiso  6511  isotilem  7265  supisolem  7267  supisoex  7268  supisoti  7269  ordiso2  7294  leisorel  11164  zfz1isolemiso  11166  seq3coll  11169  summodclem2a  12022  prodmodclem2a  12217