Theorem isof1o 5986

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 5366	. 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 2522   class class class wbr 4114   -1-1-onto->wf1o 5356   ` cfv 5357   Isom wiso 5358

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 5366

This theorem is referenced by:  isocnv2  5991  isores1  5993  isoini  5997  isoini2  5998  isoselem  5999  isose  6000  isopolem  6001  isosolem  6003  smoiso  6546  isotilem  7310  supisolem  7312  supisoex  7313  supisoti  7314  ordiso2  7339  leisorel  11234  zfz1isolemiso  11236  seq3coll  11239  summodclem2a  12092  prodmodclem2a  12287