Theorem isof1o 7359

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3067   class class class wbr 5166  –1-1-onto→wf1o 6572  ‘cfv 6573   Isom wiso 6574

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 6582

This theorem is referenced by:  isores1  7370  isomin  7373  isoini  7374  isoini2  7375  isofrlem  7376  isoselem  7377  isofr  7378  isose  7379  isofr2  7380  isopolem  7381  isosolem  7383  weniso  7390  weisoeq  7391  weisoeq2  7392  wemoiso  8014  wemoiso2  8015  smoiso  8418  smoiso2  8425  supisolem  9542  supisoex  9543  supiso  9544  ordiso2  9584  ordtypelem10  9596  oiexg  9604  oien  9607  oismo  9609  cantnfle  9740  cantnflt2  9742  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1d  9757  cantnflem1  9758  cantnffval2  9764  cantnff1o  9765  wemapwe  9766  cnfcom3lem  9772  infxpenlem  10082  iunfictbso  10183  dfac12lem2  10214  cofsmo  10338  isf34lem3  10444  isf34lem5  10447  hsmexlem1  10495  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  pwfseqlem5  10732  fz1isolem  14510  seqcoll  14513  seqcoll2  14514  isercolllem2  15714  isercoll  15716  summolem2a  15763  prodmolem2a  15982  gsumval3lem1  19947  gsumval3  19949  ordthmeolem  23830  dvne0f1  26071  dvcvx  26079  isoun  32713  nsgqusf1o  33409  erdsze2lem1  35171  fourierdlem20  46048  fourierdlem50  46077  fourierdlem51  46078  fourierdlem52  46079  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem76  46103  fourierdlem102  46129  fourierdlem114  46141