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

Theorem isof1o 5784
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 5205 . 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 3987  1-1-ontowf1o 5195  cfv 5196   Isom wiso 5197
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 5205
This theorem is referenced by:  isocnv2  5789  isores1  5791  isoini  5795  isoini2  5796  isoselem  5797  isose  5798  isopolem  5799  isosolem  5801  smoiso  6279  isotilem  6981  supisolem  6983  supisoex  6984  supisoti  6985  ordiso2  7010  leisorel  10765  zfz1isolemiso  10767  seq3coll  10770  summodclem2a  11337  prodmodclem2a  11532
  Copyright terms: Public domain W3C validator