Theorem isof1o 7264

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3044   class class class wbr 5095  –1-1-onto→wf1o 6485  ‘cfv 6486   Isom wiso 6487

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 6495

This theorem is referenced by:  isores1  7275  isomin  7278  isoini  7279  isoini2  7280  isofrlem  7281  isoselem  7282  isofr  7283  isose  7284  isofr2  7285  isopolem  7286  isosolem  7288  weniso  7295  weisoeq  7296  weisoeq2  7297  wemoiso  7915  wemoiso2  7916  smoiso  8292  smoiso2  8299  supisolem  9383  supisoex  9384  supiso  9385  ordiso2  9426  ordtypelem10  9438  oiexg  9446  oien  9449  oismo  9451  cantnfle  9586  cantnflt2  9588  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1d  9603  cantnflem1  9604  cantnffval2  9610  cantnff1o  9611  wemapwe  9612  cnfcom3lem  9618  infxpenlem  9926  iunfictbso  10027  dfac12lem2  10058  cofsmo  10182  isf34lem3  10288  isf34lem5  10291  hsmexlem1  10339  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  pwfseqlem5  10576  fz1isolem  14386  seqcoll  14389  seqcoll2  14390  isercolllem2  15591  isercoll  15593  summolem2a  15640  prodmolem2a  15859  gsumval3lem1  19802  gsumval3  19804  ordthmeolem  23704  dvne0f1  25933  dvcvx  25941  isoun  32658  nsgqusf1o  33366  erdsze2lem1  35178  fourierdlem20  46112  fourierdlem50  46141  fourierdlem51  46142  fourierdlem52  46143  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem76  46167  fourierdlem102  46193  fourierdlem114  46205