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

Theorem isof1o 6473
 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 5813 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 475 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∀wral 2896   class class class wbr 4583  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805 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 196  df-an 385  df-isom 5813 This theorem is referenced by:  isores1  6484  isomin  6487  isoini  6488  isoini2  6489  isofrlem  6490  isoselem  6491  isofr  6492  isose  6493  isofr2  6494  isopolem  6495  isosolem  6497  weniso  6504  weisoeq  6505  weisoeq2  6506  wemoiso  7044  wemoiso2  7045  smoiso  7346  smoiso2  7353  supisolem  8262  supisoex  8263  supiso  8264  ordiso2  8303  ordtypelem10  8315  oiexg  8323  oien  8326  oismo  8328  cantnfle  8451  cantnflt2  8453  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  cantnffval2  8475  cantnff1o  8476  wemapwe  8477  cnfcom3lem  8483  infxpenlem  8719  iunfictbso  8820  dfac12lem2  8849  cofsmo  8974  isf34lem3  9080  isf34lem5  9083  hsmexlem1  9131  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem9  9339  pwfseqlem5  9364  fz1isolem  13102  seqcoll  13105  seqcoll2  13106  isercolllem2  14244  isercoll  14246  summolem2a  14293  prodmolem2a  14503  gsumval3lem1  18129  gsumval3  18131  ordthmeolem  21414  dvne0f1  23579  dvcvx  23587  isoun  28862  erdsze2lem1  30439  fourierdlem20  39020  fourierdlem50  39049  fourierdlem51  39050  fourierdlem52  39051  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem76  39075  fourierdlem102  39101  fourierdlem114  39113
 Copyright terms: Public domain W3C validator