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

Theorem isof1o 5674
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 5100 . 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 270 1  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  H : A -1-1-onto-> B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wral 2391   class class class wbr 3897   -1-1-onto->wf1o 5090   ` cfv 5091    Isom wiso 5092
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 5100
This theorem is referenced by:  isocnv2  5679  isores1  5681  isoini  5685  isoini2  5686  isoselem  5687  isose  5688  isopolem  5689  isosolem  5691  smoiso  6165  isotilem  6859  supisolem  6861  supisoex  6862  supisoti  6863  ordiso2  6886  leisorel  10531  zfz1isolemiso  10533  seq3coll  10536  summodclem2a  11101
  Copyright terms: Public domain W3C validator