Theorem isof1o 7278

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3051   class class class wbr 5085  –1-1-onto→wf1o 6497  ‘cfv 6498   Isom wiso 6499

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 207  df-an 396  df-isom 6507

This theorem is referenced by:  isores1  7289  isomin  7292  isoini  7293  isoini2  7294  isofrlem  7295  isoselem  7296  isofr  7297  isose  7298  isofr2  7299  isopolem  7300  isosolem  7302  weniso  7309  weisoeq  7310  weisoeq2  7311  wemoiso  7926  wemoiso2  7927  smoiso  8302  smoiso2  8309  supisolem  9387  supisoex  9388  supiso  9389  ordiso2  9430  ordtypelem10  9442  oiexg  9450  oien  9453  oismo  9455  cantnfle  9592  cantnflt2  9594  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  cantnffval2  9616  cantnff1o  9617  wemapwe  9618  cnfcom3lem  9624  infxpenlem  9935  iunfictbso  10036  dfac12lem2  10067  cofsmo  10191  isf34lem3  10297  isf34lem5  10300  hsmexlem1  10348  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  pwfseqlem5  10586  fz1isolem  14423  seqcoll  14426  seqcoll2  14427  isercolllem2  15628  isercoll  15630  summolem2a  15677  prodmolem2a  15899  gsumval3lem1  19880  gsumval3  19882  ordthmeolem  23766  dvne0f1  25979  dvcvx  25987  addonbday  28271  isoun  32775  nsgqusf1o  33476  erdsze2lem1  35385  fourierdlem20  46555  fourierdlem50  46584  fourierdlem51  46585  fourierdlem52  46586  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem76  46610  fourierdlem102  46636  fourierdlem114  46648