Theorem isof1o 7315

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 6539	. 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 5119  –1-1-onto→wf1o 6529  ‘cfv 6530   Isom wiso 6531

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 6539

This theorem is referenced by:  isores1  7326  isomin  7329  isoini  7330  isoini2  7331  isofrlem  7332  isoselem  7333  isofr  7334  isose  7335  isofr2  7336  isopolem  7337  isosolem  7339  weniso  7346  weisoeq  7347  weisoeq2  7348  wemoiso  7970  wemoiso2  7971  smoiso  8374  smoiso2  8381  supisolem  9484  supisoex  9485  supiso  9486  ordiso2  9527  ordtypelem10  9539  oiexg  9547  oien  9550  oismo  9552  cantnfle  9683  cantnflt2  9685  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1d  9700  cantnflem1  9701  cantnffval2  9707  cantnff1o  9708  wemapwe  9709  cnfcom3lem  9715  infxpenlem  10025  iunfictbso  10126  dfac12lem2  10157  cofsmo  10281  isf34lem3  10387  isf34lem5  10390  hsmexlem1  10438  fpwwe2lem5  10647  fpwwe2lem6  10648  fpwwe2lem8  10650  pwfseqlem5  10675  fz1isolem  14477  seqcoll  14480  seqcoll2  14481  isercolllem2  15680  isercoll  15682  summolem2a  15729  prodmolem2a  15948  gsumval3lem1  19884  gsumval3  19886  ordthmeolem  23737  dvne0f1  25967  dvcvx  25975  isoun  32625  nsgqusf1o  33377  erdsze2lem1  35171  fourierdlem20  46104  fourierdlem50  46133  fourierdlem51  46134  fourierdlem52  46135  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem76  46159  fourierdlem102  46185  fourierdlem114  46197