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

Theorem isof1o 5714
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 5138 . 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 2417   class class class wbr 3935  1-1-ontowf1o 5128  cfv 5129   Isom wiso 5130
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 5138
This theorem is referenced by:  isocnv2  5719  isores1  5721  isoini  5725  isoini2  5726  isoselem  5727  isose  5728  isopolem  5729  isosolem  5731  smoiso  6205  isotilem  6899  supisolem  6901  supisoex  6902  supisoti  6903  ordiso2  6926  leisorel  10610  zfz1isolemiso  10612  seq3coll  10615  summodclem2a  11180  prodmodclem2a  11375
  Copyright terms: Public domain W3C validator