Theorem isof1o 7271

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 496	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3052   class class class wbr 5086  –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  7282  isomin  7285  isoini  7286  isoini2  7287  isofrlem  7288  isoselem  7289  isofr  7290  isose  7291  isofr2  7292  isopolem  7293  isosolem  7295  weniso  7302  weisoeq  7303  weisoeq2  7304  wemoiso  7919  wemoiso2  7920  smoiso  8295  smoiso2  8302  supisolem  9380  supisoex  9381  supiso  9382  ordiso2  9423  ordtypelem10  9435  oiexg  9443  oien  9446  oismo  9448  cantnfle  9583  cantnflt2  9585  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1d  9600  cantnflem1  9601  cantnffval2  9607  cantnff1o  9608  wemapwe  9609  cnfcom3lem  9615  infxpenlem  9926  iunfictbso  10027  dfac12lem2  10058  cofsmo  10182  isf34lem3  10288  isf34lem5  10291  hsmexlem1  10339  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  pwfseqlem5  10577  fz1isolem  14414  seqcoll  14417  seqcoll2  14418  isercolllem2  15619  isercoll  15621  summolem2a  15668  prodmolem2a  15890  gsumval3lem1  19871  gsumval3  19873  ordthmeolem  23776  dvne0f1  25989  dvcvx  25997  addonbday  28285  isoun  32790  nsgqusf1o  33491  erdsze2lem1  35401  fourierdlem20  46573  fourierdlem50  46602  fourierdlem51  46603  fourierdlem52  46604  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem76  46628  fourierdlem102  46654  fourierdlem114  46666