MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isof1o Structured version   Visualization version   GIF version

Theorem isof1o 7343
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 6570 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 497 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wral 3061   class class class wbr 5143  1-1-ontowf1o 6560  cfv 6561   Isom wiso 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 207  df-an 396  df-isom 6570
This theorem is referenced by:  isores1  7354  isomin  7357  isoini  7358  isoini2  7359  isofrlem  7360  isoselem  7361  isofr  7362  isose  7363  isofr2  7364  isopolem  7365  isosolem  7367  weniso  7374  weisoeq  7375  weisoeq2  7376  wemoiso  7998  wemoiso2  7999  smoiso  8402  smoiso2  8409  supisolem  9513  supisoex  9514  supiso  9515  ordiso2  9555  ordtypelem10  9567  oiexg  9575  oien  9578  oismo  9580  cantnfle  9711  cantnflt2  9713  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1d  9728  cantnflem1  9729  cantnffval2  9735  cantnff1o  9736  wemapwe  9737  cnfcom3lem  9743  infxpenlem  10053  iunfictbso  10154  dfac12lem2  10185  cofsmo  10309  isf34lem3  10415  isf34lem5  10418  hsmexlem1  10466  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  pwfseqlem5  10703  fz1isolem  14500  seqcoll  14503  seqcoll2  14504  isercolllem2  15702  isercoll  15704  summolem2a  15751  prodmolem2a  15970  gsumval3lem1  19923  gsumval3  19925  ordthmeolem  23809  dvne0f1  26051  dvcvx  26059  isoun  32711  nsgqusf1o  33444  erdsze2lem1  35208  fourierdlem20  46142  fourierdlem50  46171  fourierdlem51  46172  fourierdlem52  46173  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem76  46197  fourierdlem102  46223  fourierdlem114  46235
  Copyright terms: Public domain W3C validator