Theorem isof1o 7279

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3052   class class class wbr 5100  –1-1-onto→wf1o 6499  ‘cfv 6500   Isom wiso 6501

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 6509

This theorem is referenced by:  isores1  7290  isomin  7293  isoini  7294  isoini2  7295  isofrlem  7296  isoselem  7297  isofr  7298  isose  7299  isofr2  7300  isopolem  7301  isosolem  7303  weniso  7310  weisoeq  7311  weisoeq2  7312  wemoiso  7927  wemoiso2  7928  smoiso  8304  smoiso2  8311  supisolem  9389  supisoex  9390  supiso  9391  ordiso2  9432  ordtypelem10  9444  oiexg  9452  oien  9455  oismo  9457  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  14396  seqcoll  14399  seqcoll2  14400  isercolllem2  15601  isercoll  15603  summolem2a  15650  prodmolem2a  15869  gsumval3lem1  19846  gsumval3  19848  ordthmeolem  23757  dvne0f1  25985  dvcvx  25993  addonbday  28287  isoun  32791  nsgqusf1o  33508  erdsze2lem1  35416  fourierdlem20  46482  fourierdlem50  46511  fourierdlem51  46512  fourierdlem52  46513  fourierdlem63  46524  fourierdlem64  46525  fourierdlem65  46526  fourierdlem76  46537  fourierdlem102  46563  fourierdlem114  46575