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

Theorem isof1o 5829
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 5244 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 274 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wral 2468   class class class wbr 4018  1-1-ontowf1o 5234  cfv 5235   Isom wiso 5236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-isom 5244
This theorem is referenced by:  isocnv2  5834  isores1  5836  isoini  5840  isoini2  5841  isoselem  5842  isose  5843  isopolem  5844  isosolem  5846  smoiso  6327  isotilem  7035  supisolem  7037  supisoex  7038  supisoti  7039  ordiso2  7064  leisorel  10849  zfz1isolemiso  10851  seq3coll  10854  summodclem2a  11421  prodmodclem2a  11616
  Copyright terms: Public domain W3C validator