Theorem isof1o 7343

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3061   class class class wbr 5143  –1-1-onto→wf1o 6560  ‘cfv 6561   Isom wiso 6562

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 6570

This theorem is referenced by:  isores1  7354  isomin  7357  isoini  7358  isoini2  7359  isofrlem  7360  isoselem  7361  isofr  7362  isose  7363  isofr2  7364  isopolem  7365  isosolem  7367  weniso  7374  weisoeq  7375  weisoeq2  7376  wemoiso  7998  wemoiso2  7999  smoiso  8402  smoiso2  8409  supisolem  9513  supisoex  9514  supiso  9515  ordiso2  9555  ordtypelem10  9567  oiexg  9575  oien  9578  oismo  9580  cantnfle  9711  cantnflt2  9713  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1d  9728  cantnflem1  9729  cantnffval2  9735  cantnff1o  9736  wemapwe  9737  cnfcom3lem  9743  infxpenlem  10053  iunfictbso  10154  dfac12lem2  10185  cofsmo  10309  isf34lem3  10415  isf34lem5  10418  hsmexlem1  10466  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  pwfseqlem5  10703  fz1isolem  14500  seqcoll  14503  seqcoll2  14504  isercolllem2  15702  isercoll  15704  summolem2a  15751  prodmolem2a  15970  gsumval3lem1  19923  gsumval3  19925  ordthmeolem  23809  dvne0f1  26051  dvcvx  26059  isoun  32711  nsgqusf1o  33444  erdsze2lem1  35208  fourierdlem20  46142  fourierdlem50  46171  fourierdlem51  46172  fourierdlem52  46173  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem76  46197  fourierdlem102  46223  fourierdlem114  46235