Theorem isof1o 6828

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

Syntax hints:   → wi 4   ↔ wb 198  ∀wral 3117   class class class wbr 4873  –1-1-onto→wf1o 6122  ‘cfv 6123   Isom wiso 6124

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 199  df-an 387  df-isom 6132

This theorem is referenced by:  isores1  6839  isomin  6842  isoini  6843  isoini2  6844  isofrlem  6845  isoselem  6846  isofr  6847  isose  6848  isofr2  6849  isopolem  6850  isosolem  6852  weniso  6859  weisoeq  6860  weisoeq2  6861  wemoiso  7413  wemoiso2  7414  smoiso  7725  smoiso2  7732  supisolem  8648  supisoex  8649  supiso  8650  ordiso2  8689  ordtypelem10  8701  oiexg  8709  oien  8712  oismo  8714  cantnfle  8845  cantnflt2  8847  cantnfp1lem3  8854  cantnflem1b  8860  cantnflem1d  8862  cantnflem1  8863  cantnffval2  8869  cantnff1o  8870  wemapwe  8871  cnfcom3lem  8877  infxpenlem  9149  iunfictbso  9250  dfac12lem2  9281  cofsmo  9406  isf34lem3  9512  isf34lem5  9515  hsmexlem1  9563  fpwwe2lem6  9772  fpwwe2lem7  9773  fpwwe2lem9  9775  pwfseqlem5  9800  fz1isolem  13534  seqcoll  13537  seqcoll2  13538  isercolllem2  14773  isercoll  14775  summolem2a  14823  prodmolem2a  15037  gsumval3lem1  18659  gsumval3  18661  ordthmeolem  21975  dvne0f1  24174  dvcvx  24182  isoun  30027  erdsze2lem1  31731  fourierdlem20  41138  fourierdlem50  41167  fourierdlem51  41168  fourierdlem52  41169  fourierdlem63  41180  fourierdlem64  41181  fourierdlem65  41182  fourierdlem76  41193  fourierdlem102  41219  fourierdlem114  41231