Theorem isof1o 7267

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wral 3053   class class class wbr 5072  –1-1-onto→wf1o 6484  ‘cfv 6485   Isom wiso 6486

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 208  df-an 397  df-isom 6494

This theorem is referenced by:  isores1  7278  isomin  7281  isoini  7282  isoini2  7283  isofrlem  7284  isoselem  7285  isofr  7286  isose  7287  isofr2  7288  isopolem  7289  isosolem  7291  weniso  7298  weisoeq  7299  weisoeq2  7300  wemoiso  7915  wemoiso2  7916  smoiso  8292  smoiso2  8299  supisolem  9377  supisoex  9378  supiso  9379  ordiso2  9420  ordtypelem10  9432  oiexg  9440  oien  9443  oismo  9445  cantnfle  9583  cantnflt2  9585  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1d  9600  cantnflem1  9601  cantnffval2  9607  cantnff1o  9608  wemapwe  9609  cnfcom3lem  9615  infxpenlem  9926  iunfictbso  10027  dfac12lem2  10058  cofsmo  10182  isf34lem3  10288  isf34lem5  10291  hsmexlem1  10339  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  pwfseqlem5  10577  fz1isolem  14414  seqcoll  14417  seqcoll2  14418  isercolllem2  15619  isercoll  15621  summolem2a  15668  prodmolem2a  15890  gsumval3lem1  19871  gsumval3  19873  ordthmeolem  23784  dvne0f1  25997  dvcvx  26005  addonbday  28289  isoun  32794  nsgqusf1o  33499  erdsze2lem1  35431  fourierdlem20  46570  fourierdlem50  46599  fourierdlem51  46600  fourierdlem52  46601  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem76  46625  fourierdlem102  46651  fourierdlem114  46663