Theorem isof1o 5829

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 5244	. 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 2468   class class class wbr 4018   -1-1-onto->wf1o 5234   ` cfv 5235   Isom wiso 5236

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 5244

This theorem is referenced by:  isocnv2  5834  isores1  5836  isoini  5840  isoini2  5841  isoselem  5842  isose  5843  isopolem  5844  isosolem  5846  smoiso  6328  isotilem  7036  supisolem  7038  supisoex  7039  supisoti  7040  ordiso2  7065  leisorel  10852  zfz1isolemiso  10854  seq3coll  10857  summodclem2a  11424  prodmodclem2a  11619