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

Theorem isof1o 5586
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 5024 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 268 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wral 2359   class class class wbr 3845  1-1-ontowf1o 5014  cfv 5015   Isom wiso 5016
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-isom 5024
This theorem is referenced by:  isocnv2  5591  isores1  5593  isoini  5597  isoini2  5598  isoselem  5599  isose  5600  isopolem  5601  isosolem  5603  smoiso  6067  isotilem  6701  supisolem  6703  supisoex  6704  supisoti  6705  ordiso2  6728  leisorel  10242  zfz1isolemiso  10244  iseqcoll  10247  isummolem2a  10771
  Copyright terms: Public domain W3C validator