Theorem isof1o 7055

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wral 3106   class class class wbr 5030  –1-1-onto→wf1o 6323  ‘cfv 6324   Isom wiso 6325

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 210  df-an 400  df-isom 6333

This theorem is referenced by:  isores1  7066  isomin  7069  isoini  7070  isoini2  7071  isofrlem  7072  isoselem  7073  isofr  7074  isose  7075  isofr2  7076  isopolem  7077  isosolem  7079  weniso  7086  weisoeq  7087  weisoeq2  7088  wemoiso  7656  wemoiso2  7657  smoiso  7982  smoiso2  7989  supisolem  8921  supisoex  8922  supiso  8923  ordiso2  8963  ordtypelem10  8975  oiexg  8983  oien  8986  oismo  8988  cantnfle  9118  cantnflt2  9120  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1d  9135  cantnflem1  9136  cantnffval2  9142  cantnff1o  9143  wemapwe  9144  cnfcom3lem  9150  infxpenlem  9424  iunfictbso  9525  dfac12lem2  9555  cofsmo  9680  isf34lem3  9786  isf34lem5  9789  hsmexlem1  9837  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  pwfseqlem5  10074  fz1isolem  13815  seqcoll  13818  seqcoll2  13819  isercolllem2  15014  isercoll  15016  summolem2a  15064  prodmolem2a  15280  gsumval3lem1  19018  gsumval3  19020  ordthmeolem  22406  dvne0f1  24615  dvcvx  24623  isoun  30461  erdsze2lem1  32563  fourierdlem20  42769  fourierdlem50  42798  fourierdlem51  42799  fourierdlem52  42800  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem76  42824  fourierdlem102  42850  fourierdlem114  42862