Theorem isof1o 5798

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 5217	. 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 2453   class class class wbr 3998   -1-1-onto->wf1o 5207   ` cfv 5208   Isom wiso 5209

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 5217

This theorem is referenced by:  isocnv2  5803  isores1  5805  isoini  5809  isoini2  5810  isoselem  5811  isose  5812  isopolem  5813  isosolem  5815  smoiso  6293  isotilem  6995  supisolem  6997  supisoex  6998  supisoti  6999  ordiso2  7024  leisorel  10783  zfz1isolemiso  10785  seq3coll  10788  summodclem2a  11355  prodmodclem2a  11550