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

Theorem isof1o 7053
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 6340 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simplbi 500 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wral 3125   class class class wbr 5042  1-1-ontowf1o 6330  cfv 6331   Isom wiso 6332
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 209  df-an 399  df-isom 6340
This theorem is referenced by:  isores1  7064  isomin  7067  isoini  7068  isoini2  7069  isofrlem  7070  isoselem  7071  isofr  7072  isose  7073  isofr2  7074  isopolem  7075  isosolem  7077  weniso  7084  weisoeq  7085  weisoeq2  7086  wemoiso  7652  wemoiso2  7653  smoiso  7977  smoiso2  7984  supisolem  8915  supisoex  8916  supiso  8917  ordiso2  8957  ordtypelem10  8969  oiexg  8977  oien  8980  oismo  8982  cantnfle  9112  cantnflt2  9114  cantnfp1lem3  9121  cantnflem1b  9127  cantnflem1d  9129  cantnflem1  9130  cantnffval2  9136  cantnff1o  9137  wemapwe  9138  cnfcom3lem  9144  infxpenlem  9417  iunfictbso  9518  dfac12lem2  9548  cofsmo  9669  isf34lem3  9775  isf34lem5  9778  hsmexlem1  9826  fpwwe2lem6  10035  fpwwe2lem7  10036  fpwwe2lem9  10038  pwfseqlem5  10063  fz1isolem  13804  seqcoll  13807  seqcoll2  13808  isercolllem2  15002  isercoll  15004  summolem2a  15052  prodmolem2a  15268  gsumval3lem1  19004  gsumval3  19006  ordthmeolem  22385  dvne0f1  24594  dvcvx  24602  isoun  30424  erdsze2lem1  32458  fourierdlem20  42560  fourierdlem50  42589  fourierdlem51  42590  fourierdlem52  42591  fourierdlem63  42602  fourierdlem64  42603  fourierdlem65  42604  fourierdlem76  42615  fourierdlem102  42641  fourierdlem114  42653
  Copyright terms: Public domain W3C validator