Theorem isof1o 7070

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.

Step	Hyp	Ref	Expression
1		df-isom 6358	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simplbi 500	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3138   class class class wbr 5058  –1-1-onto→wf1o 6348  ‘cfv 6349   Isom wiso 6350

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 6358

This theorem is referenced by:  isores1  7081  isomin  7084  isoini  7085  isoini2  7086  isofrlem  7087  isoselem  7088  isofr  7089  isose  7090  isofr2  7091  isopolem  7092  isosolem  7094  weniso  7101  weisoeq  7102  weisoeq2  7103  wemoiso  7668  wemoiso2  7669  smoiso  7993  smoiso2  8000  supisolem  8931  supisoex  8932  supiso  8933  ordiso2  8973  ordtypelem10  8985  oiexg  8993  oien  8996  oismo  8998  cantnfle  9128  cantnflt2  9130  cantnfp1lem3  9137  cantnflem1b  9143  cantnflem1d  9145  cantnflem1  9146  cantnffval2  9152  cantnff1o  9153  wemapwe  9154  cnfcom3lem  9160  infxpenlem  9433  iunfictbso  9534  dfac12lem2  9564  cofsmo  9685  isf34lem3  9791  isf34lem5  9794  hsmexlem1  9842  fpwwe2lem6  10051  fpwwe2lem7  10052  fpwwe2lem9  10054  pwfseqlem5  10079  fz1isolem  13813  seqcoll  13816  seqcoll2  13817  isercolllem2  15016  isercoll  15018  summolem2a  15066  prodmolem2a  15282  gsumval3lem1  19019  gsumval3  19021  ordthmeolem  22403  dvne0f1  24603  dvcvx  24611  isoun  30431  erdsze2lem1  32445  fourierdlem20  42406  fourierdlem50  42435  fourierdlem51  42436  fourierdlem52  42437  fourierdlem63  42448  fourierdlem64  42449  fourierdlem65  42450  fourierdlem76  42461  fourierdlem102  42487  fourierdlem114  42499