Theorem isof1o 5716

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

Syntax hints:   -> wi 4   <-> wb 104   A.wral 2417   class class class wbr 3937   -1-1-onto->wf1o 5130   ` cfv 5131   Isom wiso 5132

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

This theorem depends on definitions:  df-bi 116  df-isom 5140

This theorem is referenced by:  isocnv2  5721  isores1  5723  isoini  5727  isoini2  5728  isoselem  5729  isose  5730  isopolem  5731  isosolem  5733  smoiso  6207  isotilem  6901  supisolem  6903  supisoex  6904  supisoti  6905  ordiso2  6928  leisorel  10612  zfz1isolemiso  10614  seq3coll  10617  summodclem2a  11182  prodmodclem2a  11377