Theorem isof1o 7301

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3045   class class class wbr 5110  –1-1-onto→wf1o 6513  ‘cfv 6514   Isom wiso 6515

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 6523

This theorem is referenced by:  isores1  7312  isomin  7315  isoini  7316  isoini2  7317  isofrlem  7318  isoselem  7319  isofr  7320  isose  7321  isofr2  7322  isopolem  7323  isosolem  7325  weniso  7332  weisoeq  7333  weisoeq2  7334  wemoiso  7955  wemoiso2  7956  smoiso  8334  smoiso2  8341  supisolem  9432  supisoex  9433  supiso  9434  ordiso2  9475  ordtypelem10  9487  oiexg  9495  oien  9498  oismo  9500  cantnfle  9631  cantnflt2  9633  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1d  9648  cantnflem1  9649  cantnffval2  9655  cantnff1o  9656  wemapwe  9657  cnfcom3lem  9663  infxpenlem  9973  iunfictbso  10074  dfac12lem2  10105  cofsmo  10229  isf34lem3  10335  isf34lem5  10338  hsmexlem1  10386  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  pwfseqlem5  10623  fz1isolem  14433  seqcoll  14436  seqcoll2  14437  isercolllem2  15639  isercoll  15641  summolem2a  15688  prodmolem2a  15907  gsumval3lem1  19842  gsumval3  19844  ordthmeolem  23695  dvne0f1  25924  dvcvx  25932  isoun  32632  nsgqusf1o  33394  erdsze2lem1  35197  fourierdlem20  46132  fourierdlem50  46161  fourierdlem51  46162  fourierdlem52  46163  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem76  46187  fourierdlem102  46213  fourierdlem114  46225