ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isof1o Unicode version

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.
StepHypRef 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 ) ) ) )
21simplbi 268 1  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator