Theorem isof1o 7329

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 6546	. 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 3077   class class class wbr 5103  –1-1-onto→wf1o 6536  ‘cfv 6537   Isom wiso 6538

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 6546

This theorem is used by:  isores1  7340  isomin  7343  isoini  7344  isoini2  7345  isofrlem  7346  isoselem  7347  isofr  7348  isose  7349  isofr2  7350  isopolem  7351  isosolem  7353  weniso  7362  weisoeq  7363  weisoeq2  7364  wemoiso  7983  wemoiso2  7984  smoiso  8363  smoiso2  8370  supisolem  9459  supisoex  9460  supiso  9461  ordiso2  9502  ordtypelem10  9514  oiexg  9522  oien  9525  oismo  9527  cantnfle  9665  cantnflt2  9667  cantnfp1lem3  9674  cantnflem1b  9680  cantnflem1d  9682  cantnflem1  9683  cantnffval2  9689  cantnff1o  9690  wemapwe  9691  cnfcom3lem  9697  infxpenlem  10085  iunfictbso  10186  dfac12lem2  10216  cofsmo  10340  isf34lem3  10446  isf34lem5  10449  hsmexlem1  10497  fpwwe2lem5  10713  fpwwe2lem6  10714  fpwwe2lem8  10716  pwfseqlem5  10741  fz1isolem  14599  seqcoll  14602  seqcoll2  14603  isercolllem2  15826  isercoll  15828  summolem2a  15874  prodmolem2a  16094  gsumval3lem1  20112  gsumval3  20114  ordthmeolem  24113  dvne0f1  26325  dvcvx  26333  addonbday  28658  isoun  33288  nsgqusf1o  33960  ordtypeon  35708  wevonprcf1o  35875  erdsze2lem1  35947  fourierdlem20  47106  fourierdlem50  47135  fourierdlem51  47136  fourierdlem52  47137  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem76  47161  fourierdlem102  47187  fourierdlem114  47199