Theorem isof1o 5586

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

Syntax hints:   -> wi 4   <-> wb 103   A.wral 2359   class class class wbr 3845   -1-1-onto->wf1o 5014   ` cfv 5015   Isom wiso 5016

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

This theorem depends on definitions:  df-bi 115  df-isom 5024

This theorem is referenced by:  isocnv2  5591  isores1  5593  isoini  5597  isoini2  5598  isoselem  5599  isose  5600  isopolem  5601  isosolem  5603  smoiso  6067  isotilem  6699  supisolem  6701  supisoex  6702  supisoti  6703  ordiso2  6726  leisorel  10238  zfz1isolemiso  10240  iseqcoll  10243  isummolem2a  10767