Theorem isof1o 7323

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3079   class class class wbr 5110  –1-1-onto→wf1o 6537  ‘cfv 6538   Isom wiso 6539

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 210  df-an 401  df-isom 6547

This theorem is referenced by:  isores1  7334  isomin  7337  isoini  7338  isoini2  7339  isofrlem  7340  isoselem  7341  isofr  7342  isose  7343  isofr2  7344  isopolem  7345  isosolem  7347  weniso  7354  weisoeq  7355  weisoeq2  7356  wemoiso  7971  wemoiso2  7972  smoiso  8350  smoiso2  8357  supisolem  9435  supisoex  9436  supiso  9437  ordiso2  9478  ordtypelem10  9490  oiexg  9498  oien  9501  oismo  9503  cantnfle  9641  cantnflt2  9643  cantnfp1lem3  9650  cantnflem1b  9656  cantnflem1d  9658  cantnflem1  9659  cantnffval2  9665  cantnff1o  9666  wemapwe  9667  cnfcom3lem  9673  infxpenlem  9998  iunfictbso  10099  dfac12lem2  10129  cofsmo  10254  isf34lem3  10360  isf34lem5  10363  hsmexlem1  10411  fpwwe2lem5  10621  fpwwe2lem6  10622  fpwwe2lem8  10624  pwfseqlem5  10649  fz1isolem  14500  seqcoll  14503  seqcoll2  14504  isercolllem2  15719  isercoll  15721  summolem2a  15768  prodmolem2a  15990  gsumval3lem1  19976  gsumval3  19978  ordthmeolem  23939  dvne0f1  26152  dvcvx  26160  addonbday  28453  isoun  33028  nsgqusf1o  33706  ordtypeon  35462  wevonprcf1o  35578  erdsze2lem1  35676  fourierdlem20  46824  fourierdlem50  46853  fourierdlem51  46854  fourierdlem52  46855  fourierdlem63  46866  fourierdlem64  46867  fourierdlem65  46868  fourierdlem76  46879  fourierdlem102  46905  fourierdlem114  46917