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

Theorem isof1o 5600
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 5037 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 269 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wral 2360   class class class wbr 3851  1-1-ontowf1o 5027  cfv 5028   Isom wiso 5029
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-isom 5037
This theorem is referenced by:  isocnv2  5605  isores1  5607  isoini  5611  isoini2  5612  isoselem  5613  isose  5614  isopolem  5615  isosolem  5617  smoiso  6081  isotilem  6755  supisolem  6757  supisoex  6758  supisoti  6759  ordiso2  6782  leisorel  10303  zfz1isolemiso  10305  iseqcoll  10308  isummolem2a  10832
  Copyright terms: Public domain W3C validator