Theorem isof1o 5854

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 5267	. 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 2475   class class class wbr 4033   -1-1-onto->wf1o 5257   ` cfv 5258   Isom wiso 5259

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 5267

This theorem is referenced by:  isocnv2  5859  isores1  5861  isoini  5865  isoini2  5866  isoselem  5867  isose  5868  isopolem  5869  isosolem  5871  smoiso  6360  isotilem  7072  supisolem  7074  supisoex  7075  supisoti  7076  ordiso2  7101  leisorel  10929  zfz1isolemiso  10931  seq3coll  10934  summodclem2a  11546  prodmodclem2a  11741