Theorem isof1o 5807

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 5225	. 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 2455   class class class wbr 4003   -1-1-onto->wf1o 5215   ` cfv 5216   Isom wiso 5217

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 5225

This theorem is referenced by:  isocnv2  5812  isores1  5814  isoini  5818  isoini2  5819  isoselem  5820  isose  5821  isopolem  5822  isosolem  5824  smoiso  6302  isotilem  7004  supisolem  7006  supisoex  7007  supisoti  7008  ordiso2  7033  leisorel  10816  zfz1isolemiso  10818  seq3coll  10821  summodclem2a  11388  prodmodclem2a  11583