Theorem isof1o 5708

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 5132	. 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 2416   class class class wbr 3929   -1-1-onto->wf1o 5122   ` cfv 5123   Isom wiso 5124

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 5132

This theorem is referenced by:  isocnv2  5713  isores1  5715  isoini  5719  isoini2  5720  isoselem  5721  isose  5722  isopolem  5723  isosolem  5725  smoiso  6199  isotilem  6893  supisolem  6895  supisoex  6896  supisoti  6897  ordiso2  6920  leisorel  10580  zfz1isolemiso  10582  seq3coll  10585  summodclem2a  11150  prodmodclem2a  11345