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

Theorem isof1o 5786
Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
Assertion
Ref Expression
isof1o (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)

Proof of Theorem isof1o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-isom 5207 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 272 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wral 2448   class class class wbr 3989  1-1-ontowf1o 5197  cfv 5198   Isom wiso 5199
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 5207
This theorem is referenced by:  isocnv2  5791  isores1  5793  isoini  5797  isoini2  5798  isoselem  5799  isose  5800  isopolem  5801  isosolem  5803  smoiso  6281  isotilem  6983  supisolem  6985  supisoex  6986  supisoti  6987  ordiso2  7012  leisorel  10772  zfz1isolemiso  10774  seq3coll  10777  summodclem2a  11344  prodmodclem2a  11539
  Copyright terms: Public domain W3C validator