Theorem isof1o 7269

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 6501	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simplbi 497	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3051   class class class wbr 5098  –1-1-onto→wf1o 6491  ‘cfv 6492   Isom wiso 6493

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 6501

This theorem is referenced by:  isores1  7280  isomin  7283  isoini  7284  isoini2  7285  isofrlem  7286  isoselem  7287  isofr  7288  isose  7289  isofr2  7290  isopolem  7291  isosolem  7293  weniso  7300  weisoeq  7301  weisoeq2  7302  wemoiso  7917  wemoiso2  7918  smoiso  8294  smoiso2  8301  supisolem  9377  supisoex  9378  supiso  9379  ordiso2  9420  ordtypelem10  9432  oiexg  9440  oien  9443  oismo  9445  cantnfle  9580  cantnflt2  9582  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1d  9597  cantnflem1  9598  cantnffval2  9604  cantnff1o  9605  wemapwe  9606  cnfcom3lem  9612  infxpenlem  9923  iunfictbso  10024  dfac12lem2  10055  cofsmo  10179  isf34lem3  10285  isf34lem5  10288  hsmexlem1  10336  fpwwe2lem5  10546  fpwwe2lem6  10547  fpwwe2lem8  10549  pwfseqlem5  10574  fz1isolem  14384  seqcoll  14387  seqcoll2  14388  isercolllem2  15589  isercoll  15591  summolem2a  15638  prodmolem2a  15857  gsumval3lem1  19834  gsumval3  19836  ordthmeolem  23745  dvne0f1  25973  dvcvx  25981  addonbday  28275  isoun  32781  nsgqusf1o  33497  erdsze2lem1  35397  fourierdlem20  46371  fourierdlem50  46400  fourierdlem51  46401  fourierdlem52  46402  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  fourierdlem76  46426  fourierdlem102  46452  fourierdlem114  46464