Theorem isof1o 7319

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3085   class class class wbr 5110  –1-1-onto→wf1o 6532  ‘cfv 6533   Isom wiso 6534

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 6542

This theorem is referenced by:  isores1  7330  isomin  7333  isoini  7334  isoini2  7335  isofrlem  7336  isoselem  7337  isofr  7338  isose  7339  isofr2  7340  isopolem  7341  isosolem  7343  weniso  7350  weisoeq  7351  weisoeq2  7352  wemoiso  7966  wemoiso2  7967  smoiso  8345  smoiso2  8352  supisolem  9430  supisoex  9431  supiso  9432  ordiso2  9473  ordtypelem10  9485  oiexg  9493  oien  9496  oismo  9498  cantnfle  9636  cantnflt2  9638  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1d  9653  cantnflem1  9654  cantnffval2  9660  cantnff1o  9661  wemapwe  9662  cnfcom3lem  9668  infxpenlem  9993  iunfictbso  10094  dfac12lem2  10124  cofsmo  10249  isf34lem3  10355  isf34lem5  10358  hsmexlem1  10406  fpwwe2lem5  10616  fpwwe2lem6  10617  fpwwe2lem8  10619  pwfseqlem5  10644  fz1isolem  14494  seqcoll  14497  seqcoll2  14498  isercolllem2  15713  isercoll  15715  summolem2a  15762  prodmolem2a  15984  gsumval3lem1  19971  gsumval3  19973  ordthmeolem  23923  dvne0f1  26136  dvcvx  26144  addonbday  28434  isoun  32984  nsgqusf1o  33665  ordtypeon  35420  wevonprcf1o  35492  erdsze2lem1  35590  fourierdlem20  46726  fourierdlem50  46755  fourierdlem51  46756  fourierdlem52  46757  fourierdlem63  46768  fourierdlem64  46769  fourierdlem65  46770  fourierdlem76  46781  fourierdlem102  46807  fourierdlem114  46819