Theorem isof1o 7194

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3064   class class class wbr 5074  –1-1-onto→wf1o 6432  ‘cfv 6433   Isom wiso 6434

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 206  df-an 397  df-isom 6442

This theorem is referenced by:  isores1  7205  isomin  7208  isoini  7209  isoini2  7210  isofrlem  7211  isoselem  7212  isofr  7213  isose  7214  isofr2  7215  isopolem  7216  isosolem  7218  weniso  7225  weisoeq  7226  weisoeq2  7227  wemoiso  7816  wemoiso2  7817  smoiso  8193  smoiso2  8200  supisolem  9232  supisoex  9233  supiso  9234  ordiso2  9274  ordtypelem10  9286  oiexg  9294  oien  9297  oismo  9299  cantnfle  9429  cantnflt2  9431  cantnfp1lem3  9438  cantnflem1b  9444  cantnflem1d  9446  cantnflem1  9447  cantnffval2  9453  cantnff1o  9454  wemapwe  9455  cnfcom3lem  9461  infxpenlem  9769  iunfictbso  9870  dfac12lem2  9900  cofsmo  10025  isf34lem3  10131  isf34lem5  10134  hsmexlem1  10182  fpwwe2lem5  10391  fpwwe2lem6  10392  fpwwe2lem8  10394  pwfseqlem5  10419  fz1isolem  14175  seqcoll  14178  seqcoll2  14179  isercolllem2  15377  isercoll  15379  summolem2a  15427  prodmolem2a  15644  gsumval3lem1  19506  gsumval3  19508  ordthmeolem  22952  dvne0f1  25176  dvcvx  25184  isoun  31034  nsgqusf1o  31601  erdsze2lem1  33165  fourierdlem20  43668  fourierdlem50  43697  fourierdlem51  43698  fourierdlem52  43699  fourierdlem63  43710  fourierdlem64  43711  fourierdlem65  43712  fourierdlem76  43723  fourierdlem102  43749  fourierdlem114  43761