Theorem isof1o 7274

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wral 3054   class class class wbr 5079  –1-1-onto→wf1o 6491  ‘cfv 6492   Isom wiso 6493

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 6501

This theorem is referenced by:  isores1  7285  isomin  7288  isoini  7289  isoini2  7290  isofrlem  7291  isoselem  7292  isofr  7293  isose  7294  isofr2  7295  isopolem  7296  isosolem  7298  weniso  7305  weisoeq  7306  weisoeq2  7307  wemoiso  7922  wemoiso2  7923  smoiso  8299  smoiso2  8306  supisolem  9384  supisoex  9385  supiso  9386  ordiso2  9427  ordtypelem10  9439  oiexg  9447  oien  9450  oismo  9452  cantnfle  9590  cantnflt2  9592  cantnfp1lem3  9599  cantnflem1b  9605  cantnflem1d  9607  cantnflem1  9608  cantnffval2  9614  cantnff1o  9615  wemapwe  9616  cnfcom3lem  9622  infxpenlem  9933  iunfictbso  10034  dfac12lem2  10065  cofsmo  10189  isf34lem3  10295  isf34lem5  10298  hsmexlem1  10346  fpwwe2lem5  10556  fpwwe2lem6  10557  fpwwe2lem8  10559  pwfseqlem5  10584  fz1isolem  14421  seqcoll  14424  seqcoll2  14425  isercolllem2  15626  isercoll  15628  summolem2a  15675  prodmolem2a  15897  gsumval3lem1  19878  gsumval3  19880  ordthmeolem  23791  dvne0f1  26004  dvcvx  26012  addonbday  28296  isoun  32801  nsgqusf1o  33506  erdsze2lem1  35438  fourierdlem20  46577  fourierdlem50  46606  fourierdlem51  46607  fourierdlem52  46608  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem76  46632  fourierdlem102  46658  fourierdlem114  46670