Theorem isof1o 7332

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3076   class class class wbr 5102  –1-1-onto→wf1o 6538  ‘cfv 6539   Isom wiso 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-isom 6548

This theorem is used by:  isores1  7343  isomin  7346  isoini  7347  isoini2  7348  isofrlem  7349  isoselem  7350  isofr  7351  isose  7352  isofr2  7353  isopolem  7354  isosolem  7356  weniso  7365  weisoeq  7366  weisoeq2  7367  wemoiso  7986  wemoiso2  7987  smoiso  8374  smoiso2  8381  supisolem  9470  supisoex  9471  supiso  9472  ordiso2  9513  ordtypelem10  9525  oiexg  9533  oien  9536  oismo  9538  cantnfle  9676  cantnflt2  9678  cantnfp1lem3  9685  cantnflem1b  9691  cantnflem1d  9693  cantnflem1  9694  cantnffval2  9700  cantnff1o  9701  wemapwe  9702  cnfcom3lem  9708  infxpenlem  10096  iunfictbso  10197  dfac12lem2  10227  cofsmo  10351  isf34lem3  10457  isf34lem5  10460  hsmexlem1  10508  fpwwe2lem5  10724  fpwwe2lem6  10725  fpwwe2lem8  10727  pwfseqlem5  10752  fz1isolem  14610  seqcoll  14613  seqcoll2  14614  isercolllem2  15839  isercoll  15841  summolem2a  15887  prodmolem2a  16107  gsumval3lem1  20125  gsumval3  20127  ordthmeolem  24126  dvne0f1  26338  dvcvx  26346  addonbday  28671  isoun  33343  nsgqusf1o  34014  ordtypeon  35771  j00smo  35945  maxssj0  35946  j0ltalephlem  35947  j0ltaleph  35948  wevonprcf1o  35962  vonf1onprcf1ac  35964  erdsze2lem1  36055  fourierdlem20  47231  fourierdlem50  47260  fourierdlem51  47261  fourierdlem52  47262  fourierdlem63  47273  fourierdlem64  47274  fourierdlem65  47275  fourierdlem76  47286  fourierdlem102  47312  fourierdlem114  47324